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}}
Updated date
make `wp_alloc l as "?"` behave as expected
!169
· created
Jul 04, 2018
by
Ralf Jung
gen_proofmode
Merged
5
updated
Jul 04, 2018
Split prettification from proof mode reduction
!170
· created
Jul 04, 2018
by
Ralf Jung
gen_proofmode
Merged
4
updated
Jul 05, 2018
Generalized proofmode
!66
· created
Sep 24, 2017
by
Robbert Krebbers
Merged
32
updated
Jul 13, 2018
BI -> Bi, to match our convention
!103
· created
Dec 20, 2017
by
Ralf Jung
gen_proofmode
Merged
2
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
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
General Invariant Tactic
!116
· created
Feb 16, 2018
by
Joseph Tassarotti
gen_proofmode
Merged
81
updated
Jul 13, 2018
rename valid -> emp_valid
!131
· created
Mar 19, 2018
by
Ralf Jung
Generalized Proofmode Merger
gen_proofmode
Merged
15
updated
Jul 13, 2018
add iSplitWith tactic for convenient conjunction monotonicity
!141
· created
Apr 23, 2018
by
Ralf Jung
gen_proofmode
T-proofmode
Closed
1
updated
Jul 13, 2018
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
Mostly Revert "change AsVal to be easier to use (like IntoVal)"
!162
· created
Jun 19, 2018
by
Ralf Jung
gen_proofmode
Closed
16
updated
Jul 13, 2018
Logically atomic triples: Notation, tactics, small example
3 of 3 checklist items completed
!163
· created
Jun 22, 2018
by
Ralf Jung
Merged
2
updated
Jul 13, 2018
Super `iModIntro` tactic that generalizes `iAlways`, `iNext`, `iModIntro`, and more
7 of 7 checklist items completed
!121
· created
Feb 23, 2018
by
Robbert Krebbers
gen_proofmode
Merged
35
updated
Jul 13, 2018
Added a new lemma to allocate fragmented ownership in unital gmaps while…
!164
· created
Jun 26, 2018
by
Jonas Kastberg
Merged
33
updated
Jul 31, 2018
Port new CI to iris-3.1.
!174
· created
Aug 30, 2018
by
Janno
iris-3.1
Merged
6
updated
Sep 03, 2018
Right-to-left evaluation order for heaplang
!178
· created
Oct 04, 2018
by
Jacques-Henri Jourdan
Merged
11
updated
Oct 04, 2018
curry wp_fork
!180
· created
Oct 04, 2018
by
Ralf Jung
Merged
1
updated
Oct 04, 2018
`Cancelable` instances for all elements of option/gmap
!127
· created
Mar 04, 2018
by
Robbert Krebbers
Merged
4
updated
Oct 04, 2018
Stronger version of adequacy that also talks about state.
!177
· created
Oct 03, 2018
by
Robbert Krebbers
Merged
5
updated
Oct 04, 2018
Support multiple steps in `PureExec`.
!179
· created
Oct 04, 2018
by
Robbert Krebbers
Merged
14
updated
Oct 07, 2018
Prev
1
…
4
5
6
7
8
9
10
11
12
…
53
Next