Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
Iris
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
122
Issues
122
List
Boards
Labels
Service Desk
Milestones
Merge Requests
18
Merge Requests
18
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Iris
Iris
Issues
Open
122
Closed
263
All
385
New issue
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}}
Due date
Priority
Created date
Last updated
Milestone due date
Due date
Popularity
Label priority
Manual
iDestruct does not handle some patterns that it probably could
#380
· opened
Nov 11, 2020
by
Tej Chajed
A-coq
C-enhancement
T-proofmode
1
0
updated
Nov 11, 2020
Make sealing consistent and document it
#379
· opened
Nov 10, 2020
by
Ralf Jung
A-coq
A-docs
C-enhancement
T-style
0
updated
Nov 10, 2020
Graveyard for obsolete code
#378
· opened
Nov 10, 2020
by
Robbert Krebbers
A-coq
4
updated
Feb 03, 2021
We have some lonely notations
#375
· opened
Nov 05, 2020
by
Ralf Jung
A-coq
C-bug
T-style
0
updated
Nov 05, 2020
Avoid sequences of "_" by adjusting lemma statements
#374
· opened
Nov 05, 2020
by
Ralf Jung
A-coq
C-enhancement
T-style
0
updated
Nov 05, 2020
Quote does not handle ⊣⊢
#373
· opened
Nov 03, 2020
by
Rodolphe Lepigre
CLOSED
1
updated
Nov 05, 2020
Add validI lemmas for discrete RAs
0 of 4 tasks completed
#371
· opened
Nov 02, 2020
by
Ralf Jung
A-coq
C-enhancement
T-algebra
1
updated
Nov 05, 2020
Add missing instances for `Duplicable` and fix `Hint Immediate` for `persistent_duplicable`
#370
· opened
Nov 02, 2020
by
Simon Friis Vindum
CLOSED
1
12
updated
Nov 04, 2020
Document HeapLang
#369
· opened
Oct 30, 2020
by
Ralf Jung
A-docs
C-enhancement
T-heap_lang
0
updated
Oct 30, 2020
Remove `inv` lemmas for agree/auth/view/etc and add `_L` variants to the ↔ lemma
#368
· opened
Oct 21, 2020
by
Robbert Krebbers
A-coq
C-enhancement
T-algebra
8
updated
Nov 04, 2020
`Export` everywhere does not permit consistent shadowing
#366
· opened
Oct 16, 2020
by
Ralf Jung
A-coq
C-project
8
updated
Nov 05, 2020
Implement typeclasses analogous to Fractional and AsFractional for discardable fractions
#364
· opened
Oct 15, 2020
by
Tej Chajed
A-coq
C-enhancement
T-base_logic
1
updated
Oct 21, 2020
Collect Iris versions required by artifacts
#363
· opened
Oct 14, 2020
by
Ralf Jung
A-infra
CLOSED
13
updated
Nov 23, 2020
gen_heap: provide init lemma for non-empty heap that provides the points-to facts
#361
· opened
Oct 13, 2020
by
Ralf Jung
A-coq
C-enhancement
T-base_logic
CLOSED
1
0
updated
Nov 10, 2020
Use the IPM to prove some example IPM extension theorems
#359
· opened
Oct 12, 2020
by
Tej Chajed
A-coq
C-enhancement
T-proofmode
3
updated
Oct 21, 2020
Add a logic-level version of gmap_view
#358
· opened
Oct 12, 2020
by
Ralf Jung
A-coq
C-enhancement
T-base_logic
1
5
updated
Dec 23, 2020
Cancelable locks
#357
· opened
Oct 12, 2020
by
Robbert Krebbers
A-theory
C-enhancement
T-heap_lang
13
updated
Oct 21, 2020
gmap_view: add fraction support to gmap_view_auth
#356
· opened
Oct 12, 2020
by
Ralf Jung
A-coq
C-enhancement
T-algebra
CLOSED
1
0
updated
Oct 21, 2020
Break dependency of algebra on base_logic
#355
· opened
Oct 06, 2020
by
Ralf Jung
A-coq
C-enhancement
T-algebra
T-base_logic
CLOSED
1
0
updated
Oct 20, 2020
Discardable camera improvements
#354
· opened
Oct 06, 2020
by
Ralf Jung
A-theory
C-enhancement
T-algebra
9
updated
Oct 09, 2020
Prev
1
2
3
4
5
6
…
20
Next