Merge requests · Iris / stdpp

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