Skip to content

Pull requests: leanprover-community/iris-lean

New pull request New
26 Open 332 Closed
26 Open 332 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Make Texan triples persistent
#568 opened Aug 4, 2026 by suhr Contributor Loading…
1 of 2 tasks
8
fix: make instMaxNatAdd a local instance
#564 opened Aug 1, 2026 by ayhon Contributor Loading…
2 tasks done
1
2
feat: make MaxNat distinct from Nat
#563 opened Jul 31, 2026 by ayhon Contributor Loading…
1 of 2 tasks
1
4
feat: port bi/lib/laterable.v and TCForall
#560 opened Jul 31, 2026 by alvinylt Contributor Loading…
2 tasks done
feat: contractive and nonexp tactics
#558 opened Jul 31, 2026 by oliversoeser Contributor Loading…
2 tasks done
1
1
feat: add total weakest preconditions
#554 opened Jul 30, 2026 by mfornet • Draft
1
feat: OFE step-indexing parametrisation, port algebra/stepindex_finite.v
#550 opened Jul 28, 2026 by alvinylt Contributor Loading…
2 tasks done
41
cleanup: post-setoid proof cleanup
#549 opened Jul 28, 2026 by Kaptch Collaborator • Draft
New semantics for resolve
#548 opened Jul 28, 2026 by maxvistrup Loading…
feat: Pure examples from HeapLang/Lib blocked The issue is blocked by a different issue.
#544 opened Jul 27, 2026 by markusdemedeiros Collaborator Loading…
2 tasks done
feat: port bi/lib/counterexamples.v (+ fix IntoWand instances)
#540 opened Jul 26, 2026 by alvinylt Contributor Loading…
10 tasks done
1
Correct handling of observations in weakestpre blocked The issue is blocked by a different issue.
#536 opened Jul 25, 2026 by maxvistrup Loading…
1
refactor: use simp_to_model for TreeMap mergeWith blocked The issue is blocked by a different issue.
#532 opened Jul 23, 2026 by ctkrug Loading…
2 tasks done
1
1
Port algebra/mra.v
#530 opened Jul 23, 2026 by lzy0505 Collaborator • Draft
2 tasks done
1
Port algebra/lib/gset_bij.v
#529 opened Jul 22, 2026 by lzy0505 Collaborator • Draft
2 tasks done
1
feat: inext with later credits
#510 opened Jul 10, 2026 by alvinylt Contributor Loading…
2 tasks done
31
feat: port List
#509 opened Jul 10, 2026 by markusdemedeiros Collaborator • Draft
2 tasks
1
feat: remaining specialisation patterns
#500 opened Jul 5, 2026 by alvinylt Contributor Loading…
2 tasks done
30
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
4
feat: add linter experiment Ideas for features that may or may not work
#445 opened Jun 4, 2026 by markusdemedeiros Collaborator • Draft
2 tasks done
3
feat: aesop_contractive tactic to solve Contractive/NonExpansive goals
#422 opened May 28, 2026 by arthur-adjedj • Draft
1
7
feat: add gmultiset camera
#187 opened Mar 20, 2026 by alok Contributor • Draft
1
feat: port max_prefix_list and mono_list foundations
#186 opened Mar 19, 2026 by alok Contributor • Draft
2
feat: port monotone number cameras
#185 opened Mar 19, 2026 by alok Contributor • Draft
2
feat: kmap
#166 opened Mar 9, 2026 by Kaptch Collaborator • Draft
1 of 3 tasks
ProTip! What’s not been updated in a month: updated:<2026-07-05.