Skip to content
GitLab
Explore
Sign in
Iris
stdpp
Merge requests
Open
9
Merged
493
Closed
47
All
549
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
Make `inv` and `oinv` work with numbers
!534
· created
Oct 27, 2023
by
Ralf Jung
Merged
10
updated
Oct 30, 2023
Make `gset` a `Definition` instead of `Notation`.
!59
· created
Mar 14, 2019
by
Robbert Krebbers
Merged
13
updated
Mar 14, 2019
Make `fmap` left associative.
!16
· created
Nov 08, 2017
by
Robbert Krebbers
Merged
1
updated
Nov 12, 2017
Make `done` work on `is_Some`.
!293
· created
Jul 03, 2021
by
Robbert Krebbers
Merged
3
updated
Jul 15, 2021
LookupTotal
2 of 2 checklist items completed
!97
· created
Sep 16, 2019
by
Dan Frumin
Merged
58
updated
Feb 11, 2020
Lookup total lemmas
!125
· created
Mar 17, 2020
by
Robbert Krebbers
Merged
4
updated
Mar 17, 2020
list.v: avoid using mangled names
!180
· created
Aug 28, 2020
by
Ralf Jung
Merged
8
updated
Aug 28, 2020
list lookup lemmas: cons, singleton
!264
· created
May 21, 2021
by
Ralf Jung
Merged
6
updated
May 25, 2021
LICENSE: Clarify which BSD license is being used
!174
· created
Jul 10, 2020
by
Paolo G. Giarrusso
Merged
0
updated
Jul 10, 2020
Let compilation under Coq 8.17 succeed without warnings.
!469
· created
Apr 24, 2023
by
Robbert Krebbers
Merged
3
updated
Apr 30, 2023
Lemmas for lookup on mjoin
!340
· created
Nov 25, 2021
by
Michael Sammler
Merged
13
updated
Nov 26, 2021
Lemmas for fin_maps
!91
· created
Aug 27, 2019
by
Michael Sammler
Merged
19
updated
Aug 29, 2019
Lemmas for `list_find` in combination with `app` and `insert`.
!134
· created
Mar 31, 2020
by
Robbert Krebbers
Merged
27
updated
May 12, 2020
Lemmas about "filter" on maps
!172
· created
Jul 07, 2020
by
Ralf Jung
Merged
14
updated
Jul 15, 2020
Lattices notation for order, join, meet, top and bot.
!23
· created
Dec 04, 2017
by
Jacques-Henri Jourdan
Merged
12
updated
Dec 05, 2017
Introduce `SingletonMS` class for multiset singletons.
!251
· created
Apr 20, 2021
by
Robbert Krebbers
Merged
26
updated
Apr 20, 2021
Introduce `set_bind` and associated lemmas + set_bind theory: revise setoid rewriting
!406
· created
Aug 09, 2022
by
Paolo G. Giarrusso
Merged
6
updated
Aug 09, 2022
introduce [default] as abbreviation for [from_option id], and use it
!32
· created
May 28, 2018
by
Ralf Jung
Merged
4
updated
May 29, 2018
Improve performance of `set_solver`
!66
· created
Apr 23, 2019
by
Robbert Krebbers
Merged
0
updated
May 25, 2021
Improve comment of `TCEq`.
!523
· created
Oct 06, 2023
by
Robbert Krebbers
Merged
3
updated
Oct 07, 2023
Prev
1
…
6
7
8
9
10
11
12
13
14
…
25
Next