Skip to content
GitLab
Explore
Sign in
Iris
stdpp
Merge requests
Open
9
Merged
486
Closed
46
All
541
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
Add tests for equiv notation
!143
· created
Apr 09, 2020
by
Paolo G. Giarrusso
Merged
2
updated
Apr 10, 2020
Add two useful lemmas
!101
· created
Oct 31, 2019
by
Amin Timany
Merged
5
updated
Nov 01, 2019
add unfolding lemma for bool_decide: bool_decide_decide
!73
· created
Jun 18, 2019
by
Ralf Jung
Merged
1
updated
Jun 18, 2019
add version of Qp_lower_bound that returns less-than facts
!186
· created
Oct 01, 2020
by
Ralf Jung
Merged
1
updated
Oct 01, 2020
add zip_with_diag and zip_diag
!215
· created
Jan 19, 2021
by
Ralf Jung
Merged
1
updated
Jan 19, 2021
add {fst,snd}_map_zip
!285
· created
Jun 23, 2021
by
Ralf Jung
Merged
3
updated
Jun 27, 2021
Added select and select_revert tactics
2 of 2 checklist items completed
!142
· created
Apr 09, 2020
by
Michael Sammler
Merged
48
updated
Jan 20, 2021
Added set lemmas about difference and union
!386
· created
Jul 13, 2022
by
Jonas Kastberg
Merged
30
updated
Sep 29, 2022
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
Added some useful lemmas about [list_subseteq]
!359
· created
Jan 12, 2022
by
Jonas Kastberg
Merged
6
updated
Jan 14, 2022
Added some useful lemmas for the [last] function
!355
· created
Jan 11, 2022
by
Jonas Kastberg
Merged
Approved
8
updated
Jan 12, 2022
Added TCForall2_Forall2 lemma
!107
· created
Jan 30, 2020
by
Michael Sammler
Merged
4
updated
Jan 30, 2020
Added two proper instances with permutations
!76
· created
Jun 25, 2019
by
Michael Sammler
Merged
18
updated
Jun 26, 2019
Additional lemmas about map_imap
!175
· created
Jul 14, 2020
by
Alix Trieu
Merged
14
updated
Jul 16, 2020
Additionally lemmas for insert, nth, take, and list_find
!55
· created
Feb 08, 2019
by
Hai Dang
Merged
1
15
updated
Feb 21, 2019
Allow compiling against "dev" version of Coq
!20
· created
Nov 29, 2017
by
Ralf Jung
Merged
4
updated
Nov 29, 2017
Allow pattern and type annotations in propset notation
!533
· created
Oct 18, 2023
by
Thibaut Pérami
Merged
35
updated
Mar 05, 2024
Also put results about `N` in a module.
!465
· created
Apr 22, 2023
by
Robbert Krebbers
Merged
2
updated
May 01, 2023
Alternative definition of `no_new_unsolved_evars` tactic
0 of 1 checklist item completed
!448
· created
Feb 17, 2023
by
Robbert Krebbers
Merged
4
updated
Mar 17, 2023
alternative implementation of mk_evar that keeps naive_solver working
!299
· created
Jul 17, 2021
by
Ralf Jung
Merged
11
updated
Jul 21, 2021
Prev
1
…
5
6
7
8
9
10
11
12
13
…
25
Next