- Aug 07, 2020
- Jul 24, 2020
-
-
Ralf Jung authored
-
- Jul 21, 2020
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jul 17, 2020
-
-
Robbert Krebbers authored
Remove `map` infix in lemmas about `dom` and `filter`. See merge request !176
-
- Jul 16, 2020
-
-
Robbert Krebbers authored
and `dom_map_filter_subseteq` → `dom_filter_subseteq` for consistency's sake. This was pointed out by @atrieu in !175 (comment 53746)
-
Robbert Krebbers authored
Additional lemmas about map_imap See merge request iris/stdpp!175
-
-
Ralf Jung authored
-
- Jul 15, 2020
-
-
Robbert Krebbers authored
Lemmas about "filter" on maps See merge request iris/stdpp!172
-
by Tej
-
Robbert Krebbers authored
prove NoDup_fmap_2_strong See merge request iris/stdpp!173
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Fix #70: add pattern variant of bind notation Closes #70 See merge request !169
-
Ralf Jung authored
-
- Jul 14, 2020
-
-
Ralf Jung authored
-
- Jul 10, 2020
-
-
Robbert Krebbers authored
LICENSE: Clarify which BSD license is being used See merge request !174
-
Paolo G. Giarrusso authored
Sister MR to iris/iris!472.
-
- Jul 02, 2020
-
-
Robbert Krebbers authored
Sketch docs for computation on [gmap], since they're a FAQ See merge request iris/stdpp!171
-
Paolo G. Giarrusso authored
Also, document why [simpl never] is not enough, with a link to an alternative design.
-
Robbert Krebbers authored
drop support for Coq 8.7 See merge request iris/stdpp!170
-
Ralf Jung authored
-
- Jul 01, 2020
-
-
Paolo G. Giarrusso authored
Use that in place of the old encoding: iris/stdpp#70 (comment 52817) Requires dropping support for Coq 8.7.
-
- Jun 29, 2020
-
-
Robbert Krebbers authored
Add solver `multiset_solver` for multisets See merge request iris/stdpp!167
-
- Jun 25, 2020
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jun 23, 2020
-
-
Robbert Krebbers authored
Prove theorem about delete of gset_to_gmap See merge request iris/stdpp!162
-
- Jun 19, 2020
- Jun 18, 2020
-
-
Robbert Krebbers authored
Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi) See merge request !164
-