- 25 Sep, 2022 1 commit
-
-
Robbert Krebbers authored
add map_fold_delete See merge request iris/stdpp!412
-
- 24 Sep, 2022 1 commit
-
-
- 23 Sep, 2022 7 commits
-
-
Robbert Krebbers authored
Add lemma `foldr_cons`. See merge request iris/stdpp!416
-
Robbert Krebbers authored
Add lemma `lookup_snoc_Some`. See merge request iris/stdpp!415
-
Robbert Krebbers authored
Add lemma `filter_app_complement`. See merge request iris/stdpp!414
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 21 Sep, 2022 1 commit
-
-
Ralf Jung authored
-
- 20 Sep, 2022 2 commits
-
-
Robbert Krebbers authored
add map_choose_or_empty See merge request iris/stdpp!413
-
Ralf Jung authored
-
- 07 Sep, 2022 1 commit
-
-
Ralf Jung authored
-
- 24 Aug, 2022 1 commit
-
-
Ralf Jung authored
Add bitvector library with automation See merge request iris/stdpp!408
-
- 23 Aug, 2022 2 commits
-
-
Michael Sammler authored
-
Michael Sammler authored
-
- 17 Aug, 2022 3 commits
-
-
Ralf Jung authored
-
Ralf Jung authored
Prepare changelog for release 1.8 See merge request iris/stdpp!410
-
Ralf Jung authored
-
- 16 Aug, 2022 2 commits
-
-
Robbert Krebbers authored
Refactor and improve documentation of feed and efeed tactics See merge request iris/stdpp!403
-
Michael Sammler authored
Refactor feed and add the feed generalize, efeed generalize, efeed inversion, and efeed destruct tactics
-
- 12 Aug, 2022 13 commits
-
-
Robbert Krebbers authored
Rename plus/minus → add/sub and put number lemmas in modules to be consistent with Coq stdlib See merge request iris/stdpp!404
-
Lennard Gäher authored
use the right list of authors.. Apply 2 suggestion(s) to 1 file(s) remove highlights
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This is similar to the trick we use for `bi` and makes it possible to import `Nat` and obtain all lemmas---i.e., those from Coq's stdlib + those from std++. Thanks to @Blaisorblade for the suggestion.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Rename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current convention for numbers.
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
add some very basic f_equiv tests See merge request iris/stdpp!409
-
Ralf Jung authored
-
- 11 Aug, 2022 6 commits
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
[list] restricted version of list_fmap_equiv_ext See merge request iris/stdpp!384
-
Michael Sammler authored
-