Commit c793b92
Sync upstream leanprover-community/iris-lean and bump to Lean 4.28.0
Merge upstream master (38 commits) bringing: Auth CMRA, HeapView, View
CMRA, internal fixpoints, coinduction, proof mode improvements (imod,
imodintro, ihave, ispecialize), IProp instances, GenMap refactor, and
Lean 4.28.0 toolchain.
Keep mathlib dependency (required by Bluebell) and bump to v4.28.0.
Fix DFrac name resolution in Permission.lean and Probability.lean
(DFrac_CMRA/op -> CMRA.op/DFrac.op) for compatibility with Lean 4.28.
Co-authored-by: Cursor <cursoragent@cursor.com>87 files changed
Lines changed: 9578 additions & 2115 deletions
File tree
- .github/workflows
- src
- Bluebell/Algebra
- Iris
- Algebra
- BI
- Lib
- Examples
- Instances
- IProp
- UPred
- ProofMode
- Patterns
- Tactics
- Std
- Tests
Some content is hidden
Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
21 | 21 | | |
22 | 22 | | |
23 | 23 | | |
24 | | - | |
| 24 | + | |
25 | 25 | | |
26 | 26 | | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
16 | 16 | | |
17 | 17 | | |
18 | 18 | | |
19 | | - | |
| 19 | + | |
20 | 20 | | |
21 | 21 | | |
22 | 22 | | |
| |||
0 commit comments