-
Notifications
You must be signed in to change notification settings - Fork 51
Pull requests: leanprover-community/iris-lean
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
refactor: remove unicode braces
#534
opened Jul 24, 2026 by
markusdemedeiros
Collaborator
Loading…
2 tasks done
refactor: use simp_to_model for TreeMap mergeWith
#532
opened Jul 23, 2026 by
ctkrug
Loading…
2 tasks done
Port
algebra/lib/ufrac_auth.v
#527
opened Jul 22, 2026 by
lzy0505
Collaborator
Loading…
2 tasks done
feat: port HeapLang heap tactics
#521
opened Jul 16, 2026 by
kdvkrs
Contributor
Loading…
2 tasks done
refactor: remove duplicate type classes in
Iris/Std/Classes.lean and reuse definitions from core libraries
#518
opened Jul 15, 2026 by
alvinylt
Contributor
Loading…
2 tasks done
feat: port
algebra/stepindex.v
#515
opened Jul 14, 2026 by
alvinylt
Contributor
Loading…
53 tasks done
feat: iframe with existential quantifiers
#511
opened Jul 12, 2026 by
alvinylt
Contributor
Loading…
2 tasks done
feat: inext with later credits
#510
opened Jul 10, 2026 by
alvinylt
Contributor
Loading…
2 tasks done
feat: remaining specialisation patterns
#500
opened Jul 5, 2026 by
alvinylt
Contributor
Loading…
2 tasks done
feat: remaining introduction patterns and case destruction patterns
#496
opened Jul 2, 2026 by
alvinylt
Contributor
Loading…
2 tasks done
feat: Experimental integration between HeapLang and Std.do (4.33.0-rc1)
experiment
Ideas for features that may or may not work
#478
opened Jun 18, 2026 by
markusdemedeiros
Collaborator
•
Draft
2 tasks
feat:
aesop_contractive tactic to solve Contractive/NonExpansive goals
#422
opened May 28, 2026 by
arthur-adjedj
•
Draft
feat: add depends on rocq concept status
#329
opened Apr 21, 2026 by
ayhon
Contributor
Loading…
3 tasks
Previous Next
ProTip!
no:milestone will show everything without a milestone.