Skip to content
GitLab
Projects
Groups
Topics
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Register
Sign in
Toggle navigation
Menu
Iris
Iris
Merge requests
Open
21
Merged
813
Closed
109
All
943
Recent searches
{{formattedKey}}
{{ title }}
{{ help }}
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
Upcoming
Started
{{title}}
None
Any
{{title}}
None
Any
{{title}}
None
Any
{{name}}
Yes
No
Yes
No
{{title}}
{{title}}
Created date
Add derived ≼ connective on the BI level.
!944
· created
Jun 05, 2023
by
Ike Mulder
14
updated
Jun 07, 2023
Add some missing internal validity and equivalence lemmas for dfrac, auth and agree
!942
· created
Jun 02, 2023
by
Ike Mulder
20
updated
Jun 06, 2023
add test for iInv with accessor variables
!937
· created
May 30, 2023
by
Ralf Jung
0
updated
May 30, 2023
Make bi fields non-canonical
!933
· created
May 26, 2023
by
Paolo G. Giarrusso
26
updated
Jun 06, 2023
Use Ltac2 to avoid unrolling tactic notations with lists.
!931
· created
May 26, 2023
by
Janno
3
14
updated
May 31, 2023
Draft: Improve validity information received from `iCombine`ing `own`s
!930
· created
May 25, 2023
by
Ike Mulder
20
updated
Jun 06, 2023
make lock spec a Class
!929
· created
May 21, 2023
by
Ralf Jung
0
updated
May 21, 2023
Add Fractional instance for AsFractional
!926
· created
May 11, 2023
by
Isaac van Bakel
33
updated
May 31, 2023
Show that for non-step indexed BIs, <pers> can trivially be inhabited.
!925
· created
May 05, 2023
by
Robbert Krebbers
14
updated
May 12, 2023
Add reference-counting reader-writer lock implementation
!923
· created
May 05, 2023
by
Isaac van Bakel
37
updated
May 31, 2023
`Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.
!916
· created
Apr 30, 2023
by
Robbert Krebbers
5
updated
May 02, 2023
Draft: Add a Strategy command for ucmra projections
!907
· created
Apr 19, 2023
by
Ike Mulder
10
updated
May 02, 2023
add fixpoint lemmas for plain and absorbing
!903
· created
Apr 01, 2023
by
William Mansky
S-waiting-for-review
10
updated
May 30, 2023
Draft: parameterize the algebra folder by the stepindex type for integration with Transfinite Iris
!888
· created
Feb 05, 2023
by
Lennard Gäher
1
74
updated
May 31, 2023
WIP: Step Update modality demonstration
!887
· created
Jan 30, 2023
by
Jonas Kastberg
1
0
updated
May 26, 2023
get rid of Z.to_nat coercion, and add some Z-based APIs: big_sepL, and HeapLang arrays
!883
· created
Jan 12, 2023
by
Ralf Jung
4
updated
Jan 12, 2023
Added fupd_plain_soundness_no_lc_strong
!857
· created
Oct 25, 2022
by
Jonas Kastberg
S-waiting-for-author
55
updated
Mar 23, 2023
Renamed/added macros to iris.sty
!851
· created
Oct 12, 2022
by
Jonas Kastberg
S-waiting-for-author
37
updated
Mar 24, 2023
Draft: move bi_persistently_emp out of BI interface, and get a basic proof mode working again
!843
· created
Aug 13, 2022
by
Ralf Jung
32
updated
May 10, 2023
Make* class tweaks
!842
· created
Aug 13, 2022
by
Ralf Jung
S-blocked
39
updated
Aug 16, 2022
Prev
1
2
Next