Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
stdpp
Merge requests
Open
2
Merged
345
Closed
31
All
378
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}}
Popularity
Priority
Created date
Updated date
Milestone due date
Popularity
Label priority
Merged date
Closed date
Title
Define [tele_arg] as a fixpoint
!368
· created
Mar 02, 2022
by
Gregory Malecha
MERGED
1
89
updated
May 16, 2022
Add lemma `set_fold_disj_union_strong`.
!267
· created
May 27, 2021
by
Robbert Krebbers
MERGED
1
8
updated
Jun 02, 2021
Avoid relying on buggy simpl never behavior
!228
· created
Feb 11, 2021
by
Tej Chajed
MERGED
1
1
updated
Feb 12, 2021
Replace unused pattern variables with underscore
!203
· created
Nov 21, 2020
by
Tej Chajed
MERGED
1
8
updated
Nov 26, 2020
Remove dead type classes and notations.
!197
· created
Oct 28, 2020
by
Robbert Krebbers
MERGED
1
5
updated
Oct 28, 2020
Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)
!164
· created
Jun 12, 2020
by
sarahzrf
MERGED
1
10
updated
Jun 18, 2020
Fix `Export` order for `length`. Remove `length` hack in strings.
!129
· created
Mar 24, 2020
by
Robbert Krebbers
MERGED
1
28
updated
Apr 11, 2020
More lemmas for `filter` w.r.t. maps
!96
· created
Sep 11, 2019
by
Robbert Krebbers
MERGED
1
2
updated
Sep 12, 2019
Additionally lemmas for insert, nth, take, and list_find
!55
· created
Feb 08, 2019
by
Hai Dang
MERGED
1
15
updated
Feb 21, 2019
Enable cumulativity for telescopes
!380
· created
May 16, 2022
by
Janno
MERGED
17
updated
May 18, 2022
Set `Hint Mode` for `FinSet`.
!379
· created
May 13, 2022
by
Robbert Krebbers
MERGED
7
updated
May 13, 2022
Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.
!378
· created
May 12, 2022
by
Robbert Krebbers
MERGED
15
updated
May 13, 2022
drop support for Coq 8.11
!377
· created
May 09, 2022
by
Ralf Jung
MERGED
2
updated
May 11, 2022
make dom domain type paremeter (D) implicit
!376
· created
May 07, 2022
by
Ralf Jung
MERGED
15
updated
May 19, 2022
Annotate telescope notations to support literal telescope arguments.
!375
· created
May 03, 2022
by
Janno
MERGED
12
updated
May 04, 2022
Add induction principle for `tele_arg`.
!374
· created
Apr 12, 2022
by
Robbert Krebbers
MERGED
1
updated
Apr 12, 2022
Add Pigeon Hole principle.
!373
· created
Apr 11, 2022
by
Robbert Krebbers
MERGED
7
updated
Apr 12, 2022
Clarify relationship between `gset_to_gmap` and `set_to_map`.
!371
· created
Mar 30, 2022
by
Robbert Krebbers
MERGED
2
updated
Apr 07, 2022
Avoid universe bumps of `gset`/`mapset` (fixes #134)
!370
· created
Mar 15, 2022
by
Robbert Krebbers
MERGED
8
updated
Mar 16, 2022
Add lemmas list_to_set_disj_elem_of_list and gmultiset_difference_disj_union_{l,r}
!369
· created
Mar 11, 2022
by
Léo Stefanesco
MERGED
5
updated
Mar 16, 2022
Prev
1
2
3
4
5
…
18
Next