Commits · master · Abhishek Anand / stdpp

03 Jul, 2021 2 commits
- Merge branch 'ralf/lookup_union_l' into 'master' · 7b2056c4
  Ralf Jung authored Jul 03, 2021
```
add lookup_union_l

See merge request iris/stdpp!292
```
  7b2056c4
- add lookup_union_l · a4dc90a9
  Ralf Jung authored Jul 03, 2021
  
  a4dc90a9
28 Jun, 2021 3 commits
- trailing newline · ddce76d7
  Ralf Jung authored Jun 28, 2021
  
  ddce76d7
- Merge branch 'changelog-addition' into 'master' · beaa69fa
  Robbert Krebbers authored Jun 28, 2021
```
Update changelog for filter extensionality lemmas

See merge request iris/stdpp!290
```
  beaa69fa
- Update changelog for filter extensionality lemmas · 951bd2eb
  Simon Friis Vindum authored Jun 28, 2021
  
  951bd2eb
27 Jun, 2021 3 commits
- changelog for sum_inhabited_r fix · 02b85368
  Ralf Jung authored Jun 27, 2021
  
  02b85368
- Merge branch 'sum-inhabited-r' into 'master' · 69e109d6
  Robbert Krebbers authored Jun 27, 2021
```
Make sum_inhabited_r not a copy of sum_inhabited_l

See merge request iris/stdpp!288
```
  69e109d6
- Make sum_inhabited_r not a copy of sum_inhabited_l · cedb9df5
  Paolo G. Giarrusso authored Jun 27, 2021
```
This existed at least as far back as
iris/stdpp@361308c7, 8 years ago.
```
  cedb9df5
26 Jun, 2021 1 commit

Merge branch 'ralf/insert_delete' into 'master' · fe3b9967

Ralf Jung authored Jun 26, 2021

rename insert_delete → insert_delete_insert; add new insert_delete matching delete_insert

See merge request iris/stdpp!287

fe3b9967

25 Jun, 2021 4 commits
- changelog · cffd6689
  Ralf Jung authored Jun 25, 2021
  
  cffd6689
- rename insert_delete → insert_delete_insert; add new insert_delete matching delete_insert · 942c669a
  Ralf Jung authored Jun 24, 2021
  
  942c669a
- Merge branch 'extra-lemmas' into 'master' · e3800ea7
  Robbert Krebbers authored Jun 25, 2021
```
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 Jun 25, 2021
  
  e22e4a76
24 Jun, 2021 5 commits
- Merge branch 'robbert/pretty_N_go_stackoverflow' into 'master' · f63bb74b
  Robbert Krebbers authored Jun 24, 2021
```
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 Jun 24, 2021 and Robbert Krebbers committed Jun 24, 2021
  
  9fefd07d
- Merge branch 'ralf/fst_snd_map_zip' into 'master' · 80c56230
  Robbert Krebbers authored Jun 24, 2021
```
add {fst,snd}_map_zip

See merge request iris/stdpp!285
```
  80c56230
- Comment. · cd778dae
  Robbert Krebbers authored Jun 24, 2021
  
  cd778dae
- Fix potential stack overflow related to `Pretty N`. · 6de30407
  Robbert Krebbers authored Jun 24, 2021
  
  6de30407
23 Jun, 2021 3 commits
- add {fst,snd}_map_zip · 6b94ffb4
  Ralf Jung authored Jun 23, 2021
  
  6b94ffb4
- deny warnings on 8.14 beta · 8eedeb59
  Ralf Jung authored Jun 23, 2021
  
  8eedeb59
- test Coq 8.14 beta branch · db699c57
  Ralf Jung authored Jun 23, 2021
  
  db699c57
19 Jun, 2021 1 commit
- Add a few set and map related lemmas · 28f8140d
  Simon Friis Vindum authored Jun 19, 2021
  
  28f8140d
18 Jun, 2021 3 commits
- Merge branch 'robbert/cross_split' into 'master' · 0a38be45
  Robbert Krebbers authored Jun 18, 2021
```
Rewrite cross split lemmas so they can more easily be used for forward reasoning.

See merge request iris/stdpp!283
```
  0a38be45
- CHANGELOG. · 45bd0293
  Robbert Krebbers authored Jun 18, 2021
  
  45bd0293
- Rewrite cross split lemmas so they can more easily be used for forward reasoning. · 13765ae7
  Robbert Krebbers authored Jun 18, 2021
  
  13765ae7
17 Jun, 2021 12 commits
- Merge branch 'robbert/setoid' into 'master' · 3bddee70
  Robbert Krebbers authored Jun 17, 2021
```
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 Jun 17, 2021
```
Add lemmas `map_intersection_filter` and `map_difference_filter`.

See merge request iris/stdpp!282
```
  5b54d2cb
- CHANGELOG. · e0c793be
  Robbert Krebbers authored Jun 16, 2021
  
  e0c793be
- Add lemmas `Permutation_equiv` and `equiv_Permutation`. · 237cfeac
  Robbert Krebbers authored Jun 16, 2021
  
  237cfeac
- Inversion lemmas for setoids on maps. · a588e72a
  Robbert Krebbers authored Jun 15, 2021
  
  a588e72a
- Rename `equiv_None` → `None_equiv_eq`, add `Some_equiv_eq` to replace prior lemmas. · c488cab8
  Robbert Krebbers authored Jun 15, 2021
  
  c488cab8
- Add lemmas `nil_equiv_eq`, `cons_equiv_eq`, `list_singleton_equiv_eq`, `app_equiv_eq`. · d6148a30
  Robbert Krebbers authored Jun 15, 2021
  
  d6148a30
- `Proper`s for `union`, `union_with`, `intersection_with`, `difference_with` on `option`. · afdc8633
  Robbert Krebbers authored Jun 15, 2021
  
  afdc8633
- Add lemma `map_filter_proper`. · 65a379f3
  Robbert Krebbers authored Jun 15, 2021
  
  65a379f3
- Add lemmas `map_intersection_filter` and `map_difference_filter`. · 14f8c75e
  Robbert Krebbers authored Jun 17, 2021
  
  14f8c75e
- Move setoid lemmas for maps to bottom of file. · 3722f090
  Robbert Krebbers authored Jun 15, 2021
  
  3722f090
- remove spurious space · 3289d1bc
  Ralf Jung authored Jun 17, 2021
  
  3289d1bc
16 Jun, 2021 3 commits
- Merge branch 'robbert/relations_alt' into 'master' · fc5f75e5
  Robbert Krebbers authored Jun 16, 2021
```
Prove more equivalences for closure operators on relations.

See merge request iris/stdpp!278
```
  fc5f75e5
- CHANGELOG. · 4d31feda
  Robbert Krebbers authored Jun 11, 2021
  
  4d31feda
- Add lemmas `rtc_nsteps_{1,2}` and `rtc_bsteps_{1,2}`. · 5c7bdf2d
  Robbert Krebbers authored Jun 16, 2021
  
  5c7bdf2d