Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Merge requests
Open
0
Merged
8
Closed
3
All
11
Subscribe to RSS feed
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}}
Updated date
Make iDestruct consume wands when it's supposed to
!591
· created
Nov 25, 2020
by
Tej Chajed
T-proofmode
MERGED
16
updated
Dec 04, 2020
Remove plainly_exist_1 from the BI axioms.
!95
· created
Dec 04, 2017
by
Jacques-Henri Jourdan
gen_proofmode
T-proofmode
MERGED
21
updated
Jul 13, 2018
Proof mode support for monotonous predicates.
!100
· created
Dec 11, 2017
by
Jacques-Henri Jourdan
janno/monfun
T-proofmode
MERGED
53
updated
Jul 13, 2018
Make `FromPure` depend on an affinity parameter
!114
· created
Feb 12, 2018
by
Jacques-Henri Jourdan
gen_proofmode
T-proofmode
MERGED
4
updated
Jul 13, 2018
rename affinely_persistently -> intuitionistically; and make it a TC-opaque definition
!130
· created
Mar 19, 2018
by
Ralf Jung
Generalized Proofmode Merger
gen_proofmode
T-proofmode
MERGED
28
updated
Mar 22, 2018
Set mode for update modalities
!115
· created
Feb 13, 2018
by
Ralf Jung
gen_proofmode
T-proofmode
MERGED
32
updated
Feb 14, 2018
Consistent handling of pure implication and forall
!104
· created
Dec 20, 2017
by
Robbert Krebbers
T-proofmode
MERGED
6
updated
Dec 21, 2017
ProofMode intro patterns: accept _ as part of variable names
!29
· created
Nov 24, 2016
by
Ralf Jung
T-proofmode
MERGED
1
updated
Nov 24, 2016