Skip to content
GitLab
Explore
Sign in
Iris
Iris
Merge requests
Open
20
Merged
909
Closed
118
All
1,047
Actions
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}}
{{title}}
Title
wp_pures: also handle [WP v]
!578
· created
Nov 09, 2020
by
Ralf Jung
Merged
5
updated
Nov 11, 2020
wp_finish: avoid making a goal unprovable
!593
· created
Nov 26, 2020
by
Ralf Jung
Merged
25
updated
Dec 05, 2020
Weakest preconditions for total program correctness
5 of 5 checklist items completed
!65
· created
Sep 24, 2017
by
Robbert Krebbers
Merged
69
updated
Jan 18, 2018
weaken BI axiom persistently_and_sep_elim and re-derive the stronger form
!119
· created
Feb 21, 2018
by
Ralf Jung
gen_proofmode
Merged
0
updated
Feb 21, 2018
Weaken axioms for BI embeddings
!137
· created
Apr 04, 2018
by
Robbert Krebbers
gen_proofmode
Merged
27
updated
Apr 09, 2018
vdash changelog
!393
· created
Mar 16, 2020
by
Ralf Jung
Merged
2
updated
Mar 16, 2020
Various improvements to iFrame
!110
· created
Feb 02, 2018
by
Robbert Krebbers
Merged
19
updated
Feb 08, 2018
various algebra lemmas
!523
· created
Sep 29, 2020
by
Ralf Jung
Merged
0
updated
Sep 29, 2020
Use |-@{...} to avoid the need for casts (in tests)
!785
· created
Apr 07, 2022
by
Gregory Malecha
Merged
3
updated
Apr 07, 2022
Use user-supplied names when destructing existentials with ? intro pattern
!479
· created
Jul 18, 2020
by
Tej Chajed
Merged
64
updated
Dec 05, 2020
Use user-supplied names in iIntros
!482
· created
Jul 21, 2020
by
Tej Chajed
Merged
8
updated
Sep 21, 2020
use term 'cost' of an instance rather than 'priority'
!833
· created
Aug 09, 2022
by
Ralf Jung
Merged
6
updated
Dec 04, 2022
Use symbol ∗ for separating conjunction.
!21
· created
Nov 01, 2016
by
Robbert Krebbers
Merged
1
11
updated
Nov 03, 2016
Use solely canonical structures for language hierarchy.
!90
· created
Nov 23, 2017
by
Robbert Krebbers
Iris 3.1
Merged
12
updated
Nov 24, 2017
Use simple variables in Makefile
!501
· created
Sep 08, 2020
by
Tej Chajed
Merged
7
updated
Sep 09, 2020
use sep. conjunction instead of conjunction for allocation lemmas
!508
· created
Sep 16, 2020
by
Ralf Jung
Merged
6
updated
Sep 16, 2020
use Qp inequality instead of frac validity for lemma statements
!558
· created
Oct 30, 2020
by
Ralf Jung
Merged
40
updated
Jan 28, 2021
use primitive projections for our mixins
!69
· created
Oct 10, 2017
by
Ralf Jung
Merged
9
updated
Oct 10, 2017
Use original pattern in iDestruct error messages
!550
· created
Oct 20, 2020
by
Tej Chajed
S-waiting-for-review
Merged
28
updated
Nov 11, 2020
Use notation N @⊆ E to avoid ambiguity.
!24
· created
Nov 18, 2016
by
Robbert Krebbers
Merged
21
updated
Nov 23, 2016
Prev
1
2
3
4
5
…
46
Next