Commits · 942c669ae8c15c2e3948734d67dd53838b1f2edf · Adam / stdpp

Jun 25, 2021
- rename insert_delete → insert_delete_insert; add new insert_delete matching delete_insert · 942c669a
  Ralf Jung authored 3 years ago
  
  942c669a
- Merge branch 'extra-lemmas' into 'master' · e3800ea7
  Robbert Krebbers authored 3 years ago
  
  Add a few set and map related lemmas See merge request iris/stdpp!284
  e3800ea7
- Add changelog entry and make small tweaks · e22e4a76
  Simon Friis Vindum authored 3 years ago
  
  e22e4a76
Jun 24, 2021
- Merge branch 'robbert/pretty_N_go_stackoverflow' into 'master' · f63bb74b
  Robbert Krebbers authored 3 years ago
  
  Fix potential stack overflow related to `Pretty N`. See merge request iris/stdpp!286
  f63bb74b
- Apply 1 suggestion(s) to 1 file(s) · 9fefd07d
  Ralf Jung authored 3 years ago and Robbert Krebbers committed 3 years ago
  
  9fefd07d
- Merge branch 'ralf/fst_snd_map_zip' into 'master' · 80c56230
  Robbert Krebbers authored 3 years ago
  
  add {fst,snd}_map_zip See merge request iris/stdpp!285
  80c56230
- Comment. · cd778dae
  Robbert Krebbers authored 3 years ago
  
  cd778dae
- Fix potential stack overflow related to `Pretty N`. · 6de30407
  Robbert Krebbers authored 3 years ago
  
  6de30407
Jun 23, 2021
- add {fst,snd}_map_zip · 6b94ffb4
  Ralf Jung authored 3 years ago
  
  6b94ffb4
- deny warnings on 8.14 beta · 8eedeb59
  Ralf Jung authored 3 years ago
  
  8eedeb59
- test Coq 8.14 beta branch · db699c57
  Ralf Jung authored 3 years ago
  
  db699c57
Jun 19, 2021
- Add a few set and map related lemmas · 28f8140d
  Simon Friis Vindum authored 3 years ago
  
  28f8140d
Jun 18, 2021
- Merge branch 'robbert/cross_split' into 'master' · 0a38be45
  Robbert Krebbers authored 3 years ago
  
  Rewrite cross split lemmas so they can more easily be used for forward reasoning. See merge request !283
  0a38be45
- CHANGELOG. · 45bd0293
  Robbert Krebbers authored 3 years ago
  
  45bd0293
- Rewrite cross split lemmas so they can more easily be used for forward reasoning. · 13765ae7
  Robbert Krebbers authored 3 years ago
  
  13765ae7
Jun 17, 2021
- Merge branch 'robbert/setoid' into 'master' · 3bddee70
  Robbert Krebbers authored 3 years ago
  
  Various setoids lemmas for maps, lists, and option See merge request iris/stdpp!281
  3bddee70
- Merge branch 'robbert/intersection_difference_filter' into 'master' · 5b54d2cb
  Robbert Krebbers authored 3 years ago
  
  Add lemmas `map_intersection_filter` and `map_difference_filter`. See merge request iris/stdpp!282
  5b54d2cb
- CHANGELOG. · e0c793be
  Robbert Krebbers authored 3 years ago
  
  e0c793be
- Add lemmas `Permutation_equiv` and `equiv_Permutation`. · 237cfeac
  Robbert Krebbers authored 3 years ago
  
  237cfeac
- Inversion lemmas for setoids on maps. · a588e72a
  Robbert Krebbers authored 3 years ago
  
  a588e72a
- Rename `equiv_None` → `None_equiv_eq`, add `Some_equiv_eq` to replace prior lemmas. · c488cab8
  Robbert Krebbers authored 3 years ago
  
  c488cab8
- Add lemmas `nil_equiv_eq`, `cons_equiv_eq`, `list_singleton_equiv_eq`, `app_equiv_eq`. · d6148a30
  Robbert Krebbers authored 3 years ago
  
  d6148a30
- `Proper`s for `union`, `union_with`, `intersection_with`, `difference_with` on `option`. · afdc8633
  Robbert Krebbers authored 3 years ago
  
  afdc8633
- Add lemma `map_filter_proper`. · 65a379f3
  Robbert Krebbers authored 3 years ago
  
  65a379f3
- Add lemmas `map_intersection_filter` and `map_difference_filter`. · 14f8c75e
  Robbert Krebbers authored 3 years ago
  
  14f8c75e
- Move setoid lemmas for maps to bottom of file. · 3722f090
  Robbert Krebbers authored 3 years ago
  
  3722f090
- remove spurious space · 3289d1bc
  Ralf Jung authored 3 years ago
  
  3289d1bc
Jun 16, 2021
- Merge branch 'robbert/relations_alt' into 'master' · fc5f75e5
  Robbert Krebbers authored 3 years ago
  
  Prove more equivalences for closure operators on relations. See merge request iris/stdpp!278
  fc5f75e5
- CHANGELOG. · 4d31feda
  Robbert Krebbers authored 3 years ago
  
  4d31feda
- Add lemmas `rtc_nsteps_{1,2}` and `rtc_bsteps_{1,2}`. · 5c7bdf2d
  Robbert Krebbers authored 3 years ago
  
  5c7bdf2d
Jun 15, 2021
- Prove more equivalences for closure operators on relations. · 40a0487a
  Robbert Krebbers authored 3 years ago
  
  As part of this: turn `rtc_nsteps` and `rtc_bsteps` into ``s. The `_list` lemmas were proposed by @jules and he provided an initial proof specific to `rtc`.
  40a0487a
- Merge branch 'robbert/misc_map' into 'master' · ed5b8dd4
  Robbert Krebbers authored 3 years ago
  
  Misc lemmas for maps See merge request iris/stdpp!280
  ed5b8dd4
- Add lemmas `merge_empty_l` and `merge_empty_r`. · deebe088
  Robbert Krebbers authored 3 years ago
  
  deebe088
- Add lemma `map_filter_lookup`. · e46cc03a
  Robbert Krebbers authored 3 years ago
  
  e46cc03a
- Add lemma `map_fmap_singleton_inv`. · e2a38b9a
  Robbert Krebbers authored 3 years ago
  
  e2a38b9a
Jun 11, 2021
- Merge branch 'robbert/head_tail' into 'master' · b2a8bf65
  Robbert Krebbers authored 3 years ago
  
  Misc improvements to `head` and `tail` functions for lists See merge request iris/stdpp!277
  b2a8bf65
- Add tests for `simpl` on `last`. · 195c8282
  Robbert Krebbers authored 3 years ago
  
  195c8282
- Comment about `head` and `tail` notations. · e1e8316a
  Robbert Krebbers authored 3 years ago
  
  e1e8316a
- CHANGELOG. · 7d8bf699
  Robbert Krebbers authored 3 years ago
  
  7d8bf699
- Add lemmas for `head` similar to those for `tail`. · 40d86146
  Robbert Krebbers authored 3 years ago
  
  40d86146