Commits · d85f1a2487f62be1daddba5be6b2db77177fbafe · Adam / Iris

01 Feb, 2021 3 commits
- changelog · d85f1a24
  Ralf Jung authored Feb 01, 2021
  
  d85f1a24
- fix instance rename fallout · 5b8bed2a
  Ralf Jung authored Jan 28, 2021
  
  5b8bed2a
- Rename monoid-related operational typeclass instances to include the suffix '_instance' · 7ba65e10
  Ralf Jung authored Jan 28, 2021
```
This was done using the following sed script:
sed -i -E 's/Instance ([a-zA-Z0-9_]+)( .*: (Op|P?Core|ValidN?|Unit) )/Instance \1_instance\2/' $(find iris/algebra -name "*.v")
```
  7ba65e10
29 Jan, 2021 8 commits
- Merge branch 'ralf/less-coerce' into 'master' · c4ea27fb
  Ralf Jung authored Jan 29, 2021
```
only locally make uPred_holds a coercion

See merge request iris/iris!631
```
  c4ea27fb
- only locally make siProp_holds a coercion · 2c1dd026
  Ralf Jung authored Jan 29, 2021
  
  2c1dd026
- only locally make uPred_holds a coercion · 48068213
  Ralf Jung authored Jan 29, 2021
  
  48068213
- Merge branch 'ralf/big-wand' into 'master' · 2b559473
  Robbert Krebbers authored Jan 29, 2021
```
add _wand lemmas for big-ops

See merge request iris/iris!630
```
  2b559473
- add _wand lemmas for big-ops · 3670501d
  Ralf Jung authored Jan 29, 2021
  
  3670501d
- Merge branch 'ralf/big_sepM_filter' into 'master' · 763a1b41
  Ralf Jung authored Jan 29, 2021
```
add big_sepM_filter

See merge request iris/iris!627
```
  763a1b41
- changelog · 9e72d10e
  Ralf Jung authored Jan 29, 2021
  
  9e72d10e
- reorder arguments to remain consistent with what was already there before · 31afcab0
  Ralf Jung authored Jan 29, 2021
  
  31afcab0
28 Jan, 2021 2 commits
- Bump std++. · bc58a332
  Robbert Krebbers authored Jan 28, 2021
  
  bc58a332
- Generalize `big_opM_filter'` and `big_opS_filter'` to arbitrary monoids, and... · 6704f088
  Robbert Krebbers authored Jan 28, 2021
```
Generalize `big_opM_filter'` and `big_opS_filter'` to arbitrary monoids, and make arguments consistent.
```
  6704f088
27 Jan, 2021 3 commits
- Merge branch 'ci/rodolphe/tactics' into 'master' · cb569d36
  Ralf Jung authored Jan 27, 2021
```
Add [iSelect], and various tactics based on it

See merge request !625
```
  cb569d36
- Add [iSelect], and various tactics based on it · 6e94dcaa
  Rodolphe Lepigre authored Jan 27, 2021 and Ralf Jung committed Jan 27, 2021
  
  6e94dcaa
- add big_sepM_filter · 70ec4cba
  Ralf Jung authored Jan 27, 2021
  
  70ec4cba
26 Jan, 2021 20 commits
- Merge branch 'ralf/big_sepS_elem_of_acc_impl' into 'master' · 79f2f36f
  Ralf Jung authored Jan 26, 2021
```
add big_sepS_elem_of_acc_impl

See merge request iris/iris!570
```
  79f2f36f
- changelog · 1464e6d3
  Ralf Jung authored Jan 26, 2021
  
  1464e6d3
- formatting and implicit agument nits · 6dab90d3
  Ralf Jung authored Jan 26, 2021
  
  6dab90d3
- Add variants for all big ops. · 9b53da41
  Robbert Krebbers authored Jan 17, 2021 and Ralf Jung committed Jan 26, 2021
  
  9b53da41
- add big_sepS_elem_of_acc_impl · f56f3834
  Ralf Jung authored Nov 04, 2020
  
  f56f3834
- Merge branch 'ralf/big_sepL' into 'master' · 69cd8d4f
  Robbert Krebbers authored Jan 26, 2021
```
some big_sepL lemmas

See merge request !620
```
  69cd8d4f
- add changelog · 3d1cf0c2
  Ralf Jung authored Jan 26, 2021
  
  3d1cf0c2
- do some proofs via rewrite instead of induction · d1d214ab
  Ralf Jung authored Jan 20, 2021
  
  d1d214ab
- Add `big_sepL_sepL2_2` and `big_sepM_sepM2_2`. · adf8ecd2
  Robbert Krebbers authored Jan 19, 2021
  
  adf8ecd2
- Add lemma `big_sepL_sepL2_diag` and `big_sepM_sepM2_diag`. · a92bf1dd
  Robbert Krebbers authored Jan 17, 2021
  
  a92bf1dd
- Generalize `big_sepL_sepL2` to become bidirectional, add same kind of lemma for maps. · d920fcd4
  Robbert Krebbers authored Jan 17, 2021
  
  d920fcd4
- Add `zip`/`zip_with` lemmas for big ops over maps. · 0e5917cf
  Robbert Krebbers authored Jan 17, 2021
  
  0e5917cf
- Generalize lemma `big_sepL2_app_inv` and use that to prove `big_sepL2_snoc`. · ee535aa2
  Robbert Krebbers authored Jan 17, 2021
  
  ee535aa2
- Move header to the right place. · 790f7f33
  Robbert Krebbers authored Jan 17, 2021
  
  790f7f33
- Generalize big_op lemmas for `zip` to `zip_with` and general monoids. · 9cdd69a9
  Robbert Krebbers authored Jan 17, 2021
  
  9cdd69a9
- rename new lemma to big_sepL_sepL2 · 452bcbc6
  Ralf Jung authored Jan 16, 2021
  
  452bcbc6
- apply review feedback · e8f429b9
  Ralf Jung authored Jan 15, 2021
  
  e8f429b9
- add snoc lemmas to big-list ops · 4fe7821b
  Ralf Jung authored Jan 12, 2021
  
  4fe7821b
- some big_sepL lemmas · 596e8767
  Ralf Jung authored Jan 12, 2021
  
  596e8767
- Merge branch 'robbert/wp_apply_pure' into 'master' · a26cf167
  Ralf Jung authored Jan 26, 2021
```
Make `wp_apply` perform `wp_pure` in small steps until the lemma matches the goal.

See merge request !587
```
  a26cf167
25 Jan, 2021 3 commits
- Fix CHANGELOG. · d41f8ad5
  Robbert Krebbers authored Jan 25, 2021
  
  d41f8ad5
- Merge branch 'robbert/removeT' into 'master' · 21b7ffa1
  Robbert Krebbers authored Jan 25, 2021
```
Rename `ofeT`→`ofe`, `cmraT`→`cmra`, and `ucmraT`→`ucmra`.

See merge request iris/iris!623
```
  21b7ffa1
- Merge branch 'ralf/mono-nat' into 'master' · 6451b77c
  Ralf Jung authored Jan 25, 2021
```
add mono_nat_auth_lb

See merge request iris/iris!605
```
  6451b77c
23 Jan, 2021 1 commit
- Fix. · 7bee0997
  Robbert Krebbers authored Jan 23, 2021
  
  7bee0997