Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: add Stream'.pmap & Seq'.pmap #14401

Closed
wants to merge 63 commits into from
Closed

feat: add Stream'.pmap & Seq'.pmap #14401

wants to merge 63 commits into from

Conversation

Komyyy
Copy link
Collaborator

@Komyyy Komyyy commented Jul 4, 2024 •
edited
Loading

Komyyy and others added 30 commits May 26, 2024 19:43
@Komyyy
rename Stream'.Seq to Seq'
e3783f3
@Komyyy
overview.yaml
8f49314
@Komyyy
nolints
11eeb67
@Komyyy
Merge branch 'master' into Komyyy/Seq'
e9ef163
@Komyyy
add cases_eliminators to Seq'.recOn
c601771
@Komyyy
Merge branch 'master' into Komyyy/Seq'
a0f4906
@Komyyy
Merge branch 'Komyyy/Seq'' into Komyyy/Seq'.recOn
b9a9dce
@Komyyy
Merge branch 'master' into Komyyy/Seq'
4a1a4df
@Komyyy
Merge branch 'Komyyy/Seq'' into Komyyy/Seq'.recOn
fe0e627
@Komyyy
omit Seq'.recOn
f65ea60
@Komyyy
Merge branch 'master' into Komyyy/Seq'
c237904
@Komyyy
Merge branch 'Komyyy/Seq'' into Komyyy/Seq'.recOn
e1bc584
@Komyyy
make Seq'.mem_rec_on more useful
938069a
@Komyyy
prove ∀ a ∈ (s : Seq' α), p a using coinduction
1452a79
@Komyyy
Merge branch 'master' into Komyyy/Seq'
67bb925
@Komyyy
Merge branch 'Komyyy/Seq'' into Komyyy/Seq'.recOn
bf2e434
@Komyyy
Merge branch 'Komyyy/Seq'.recOn' into Seq'.mem_rec_on
e0b112d
@Komyyy
Merge branch 'Seq'.mem_rec_on' into Komyyy/Seq'.all_of_allTest
690999f
@Komyyy
more simple
fe20592
@Komyyy
add Stream'.pmap & Seq'.pmap
5837875
@Komyyy
Merge branch 'master' into Komyyy/Seq'
71ebf63
@Komyyy
Merge branch 'Komyyy/Seq'' into Komyyy/Seq'.recOn
4877811
@Komyyy
Merge branch 'Komyyy/Seq'.recOn' of https://github.com/leanprover-com…
2d03329 
…munity/mathlib4 into Komyyy/Seq'.recOn
@Komyyy
Merge branch 'Komyyy/Seq'.recOn' into Seq'.mem_rec_on
24844d7
@Komyyy
Merge branch 'Seq'.mem_rec_on' into Komyyy/Seq'.all_of_allTest
270b6ef
@Komyyy
remove intros
a73274c
@Komyyy
Merge branch 'Komyyy/Seq'.recOn' into Seq'.mem_rec_on
54b2f08
@Komyyy
Merge branch 'Seq'.mem_rec_on' into Komyyy/Seq'.all_of_allTest
27c1601
@Komyyy
Merge branch 'master' into Komyyy/Seq'
23579d8
@Komyyy
Merge branch 'Komyyy/Seq'' into Komyyy/Seq'.recOn
4573b31
@Komyyy Komyyy removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 21, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 24, 2024
@Komyyy Komyyy removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 4, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 5, 2024
@grunweg grunweg added the t-data Data (lists, quotients, numbers, etc) label Aug 15, 2024
@Komyyy
Copy link
Collaborator Author

Komyyy commented Dec 4, 2024 •
edited
Loading

❗This project is temporarily frozen, PRs are all closed for a moment (I keep the branch as it may be revived someday). Detail

@Komyyy Komyyy closed this Dec 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-data Data (lists, quotients, numbers, etc) WIP Work in progress
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@Komyyy @grunweg @leanprover-community-mathlib4-bot