Skip to content

Pull requests: leanprover-community/iris-lean

New pull request New
30 Open 285 Closed
30 Open 285 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

feat: notations for internalCmraValid, internalEq, internalIncluded
#519 opened Jul 16, 2026 by alvinylt Contributor Loading…
2 tasks done
feat: deprecate Iris/Std/Classes.lean and reuse definitions from core libraries
#518 opened Jul 15, 2026 by alvinylt Contributor Loading…
1 of 2 tasks
1
feat: port HeapLang pure step tactics
#516 opened Jul 14, 2026 by kdvkrs Loading…
2 tasks done
3
feat: port algebra/stepindex.v
#515 opened Jul 14, 2026 by alvinylt Contributor • Draft
52 of 53 tasks
feat: more expressive semiOutParam attribute for ipm_class declarations
#513 opened Jul 13, 2026 by alvinylt Contributor Loading…
2 tasks done
feat: iframe with existential quantifiers
#511 opened Jul 12, 2026 by alvinylt Contributor Loading…
2 tasks done
1
feat: inext with later credits
#510 opened Jul 10, 2026 by alvinylt Contributor Loading…
2 tasks done
feat: port List
#509 opened Jul 10, 2026 by markusdemedeiros Collaborator • Draft
2 tasks
1
Fix: simp and rw sometimes exit the ProofMode
#506 opened Jul 9, 2026 by lzy0505 Collaborator Loading…
2 tasks done
1
1
feat: istart with BI specified
#505 opened Jul 8, 2026 by alvinylt Contributor Loading…
2 tasks done
feat: Port dyn_reservation_map.v
#504 opened Jul 7, 2026 by lzy0505 Collaborator Loading…
2 tasks done
1
feat: saved propositions
#503 opened Jul 7, 2026 by markusdemedeiros Collaborator Loading…
2 tasks done
1
1
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: ieval, isimp and iunfold
#490 opened Jun 30, 2026 by alvinylt Contributor Loading…
2 tasks done
feat: iaccu
#487 opened Jun 28, 2026 by alvinylt Contributor Loading…
2 tasks done
1
feat: Experimental integration between HeapLang and Std.do experiment Ideas for features that may or may not work
#478 opened Jun 18, 2026 by markusdemedeiros Collaborator • Draft
2 tasks
feat: HeapLang completeness
#477 opened Jun 18, 2026 by markusdemedeiros Collaborator • Draft
2 tasks
feat: Completeness for generic logics
#476 opened Jun 18, 2026 by markusdemedeiros Collaborator Loading…
2 tasks
feat: iinv
#470 opened Jun 16, 2026 by alvinylt Contributor Loading…
2 tasks done
1
feat: add linter
#445 opened Jun 4, 2026 by markusdemedeiros Collaborator • Draft
2 tasks done
3
feat: iinduction
#430 opened May 31, 2026 by alvinylt Contributor Loading…
10 tasks done
1
86
feat: aesop_contractive tactic to solve Contractive/NonExpansive goals
#422 opened May 28, 2026 by arthur-adjedj • Draft
1
7
feat: add depends on rocq concept status
#329 opened Apr 21, 2026 by ayhon Contributor Loading…
3 tasks
1
3
feat: add gmultiset camera
#187 opened Mar 20, 2026 by alok Contributor • Draft
1
ProTip! Type g i on any issue or pull request to go back to the issue listing page.