Skip to content

feat: Port algebra/monoid.v and algebra/big_op.v #132

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

Merged
lzy0505 merged 14 commits into from
Mar 16, 2026
Merged

feat: Port algebra/monoid.v and algebra/big_op.v #132

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
7b97935
feat: Add BigOp algebra and monoid definitions
lzy0505 Mar 2, 2026
0ca2cac
Clean up
lzy0505 Mar 4, 2026
d8215c1
Update PORTING.md
lzy0505 Mar 4, 2026
fd9c653
Add notations
lzy0505 Mar 5, 2026
8293356
chore: cleanup monoid
markusdemedeiros Mar 10, 2026
a553080
chore: cleanup bigOpL (checkpoint)
markusdemedeiros Mar 10, 2026
d477833
chore: cleanup names (checkpoint)
markusdemedeiros Mar 12, 2026
a939d90
checkpoint
markusdemedeiros Mar 12, 2026
40c62c1
checkpoint
markusdemedeiros Mar 13, 2026
1ee12f9
more refactoring
markusdemedeiros Mar 13, 2026
4387347
chore: cleanup
markusdemedeiros Mar 14, 2026
a5611b7
chore: cleanup pass
markusdemedeiros Mar 16, 2026
1d703ed
chore: cleanup
markusdemedeiros Mar 16, 2026
5bc41cc
Merge branch 'master' into zliu/algebra-bigop-monoid
markusdemedeiros Mar 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 6 additions & 4 deletions PORTING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,11 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
- [x] Updates
- [x] Functors
- [ ] `big_op.v`
- TBD (Zongyuan?)
- [x] Lists
- [x] Maps
- [ ] Sets
- [ ] Multisets
- [ ] Homomorphisms
- [ ] `cmra.v`
- [x] Lemmas
- [ ] Total CMRA construction
Expand Down Expand Up @@ -72,7 +76,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
- [ ] `max_prefix_list.v`
- [ ] Lemmas
- [ ] Functors
- [ ] `monoid.v`
- [x] `monoid.v`
- [ ] `mra.v`
- [x] `numbers.v`
- [ ] `ofe.v`
Expand Down Expand Up @@ -430,5 +434,3 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
- [ ] `language.v`
- [ ] `ectx_language.v`
- [ ] `ectxi_language.v`


Loading
Loading