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
116
Issues
116
List
Boards
Labels
Service Desk
Milestones
Merge Requests
20
Merge Requests
20
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
116
Closed
261
All
377
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}}
Created date
Priority
Created date
Last updated
Milestone due date
Due date
Popularity
Label priority
Manual
`iRename` fails with bad error message when not in proof mode
#397
· opened
Jan 12, 2021
by
Robbert
1
updated
Jan 12, 2021
Intro pattern `>` has wrong behavior with side-conditions of `iMod`
#396
· opened
Jan 12, 2021
by
Robbert
3
updated
Jan 12, 2021
Generalize frac to dfrac in view camera
#395
· opened
Jan 04, 2021
by
Simon Friis Vindum
A-coq
C-enhancement
T-algebra
1
2
updated
Jan 16, 2021
Document relation between Discrete and Timeless (in appendix?)
#394
· opened
Dec 23, 2020
by
Paolo G. Giarrusso
A-docs
T-algebra
T-base_logic
0
updated
Jan 06, 2021
Masks in step-taking fupd notation
#392
· opened
Dec 10, 2020
by
Ralf Jung
A-theory
C-enhancement
T-base_logic
1
0
updated
Dec 10, 2020
Add append-only list RA to Iris
#391
· opened
Dec 08, 2020
by
Ralf Jung
A-coq
C-enhancement
T-algebra
T-base_logic
0
updated
Dec 09, 2020
Citation guide
#389
· opened
Dec 06, 2020
by
Tej Chajed
A-docs
1
updated
Dec 08, 2020
reshape_expr does not recognize `fill`
#385
· opened
Nov 27, 2020
by
Ralf Jung
A-coq
C-enhancement
T-heap_lang
0
updated
Dec 05, 2020
Make sure we have Hint Mode for every typeclass
0 of 1 task completed
#381
· opened
Nov 12, 2020
by
Ralf Jung
A-coq
C-bug
T-style
0
updated
Nov 12, 2020
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
A-coq
3
updated
Dec 07, 2020
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
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
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
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
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
Prev
1
2
3
4
5
6
Next