Commits · master · Iris / transfinite

14 Apr, 2021 1 commit
- update license · 0ad25f97
  Lennard Gäher authored Apr 14, 2021
  
  0ad25f97
08 Dec, 2020 1 commit
- gstep rule · 904f6c86
  Simon Spies authored Dec 08, 2020
  
  904f6c86
28 Nov, 2020 1 commit
- Update README.md · c2247c3a
  Lennard Gäher authored Nov 28, 2020
  
  c2247c3a
24 Nov, 2020 3 commits
- use non-timing runner · 4d112423
  Ralf Jung authored Nov 24, 2020
  
  4d112423
- add CI back in · 52fe6ce9
  Lennard Gäher authored Nov 24, 2020
  
  52fe6ce9
- rebase transfinite iris · 0c58544d
  Lennard Gäher authored Nov 24, 2020
  
  0c58544d
22 Jul, 2019 1 commit
- mention how to use iLöb for recursive functions · 75a18932
  Ralf Jung authored Jul 22, 2019
  
  75a18932
14 Jul, 2019 4 commits
- Merge branch 'big_sepL2_app_inv_2' into 'master' · e1d90815
  Robbert Krebbers authored Jul 14, 2019
```
Add `big_sepL2_app_inv_2`.

See merge request iris!292
```
  e1d90815
- Rename `big_sepL2_app_inv_2` -> `big_sepL2_app_inv`. · 19e02ccc
  Dan Frumin authored Jul 14, 2019 and Robbert Krebbers committed Jul 14, 2019
```
And shorten the proof.
```
  19e02ccc
- Merge branch 'head_prim_fill_reducible' into 'master' · ff179bf5
  Robbert Krebbers authored Jul 14, 2019
```
Add `head_prim_fill_reducible`.

See merge request iris!293
```
  ff179bf5
- Add `head_prim_fill_reducible`. · 6e7d8b43
  Dan Frumin authored Jul 14, 2019 and Robbert Krebbers committed Jul 14, 2019
```
A more general implication from `head_reducible` to `reducible`.
```
  6e7d8b43
13 Jul, 2019 7 commits
- Merge branch 'sigTO_proper_projs' into 'master' · f1cead30
  Robbert Krebbers authored Jul 13, 2019
```
Mark projections for sigTO as NonExpansive and Proper

See merge request iris!285
```
  f1cead30
- Mark projections for sigTO as NonExpansive and Proper · 8c68ae86
  Paolo G. Giarrusso authored Jul 13, 2019 and Robbert Krebbers committed Jul 13, 2019
  
  8c68ae86
- proper link and less Rust ;) · 49a876b6
  Ralf Jung authored Jul 13, 2019
  
  49a876b6
- erasure is in iris/examples · 2663ac37
  Ralf Jung authored Jul 13, 2019
  
  2663ac37
- Weaken premise of `gmultiset_local_update_dealloc`. · 06f3218d
  Robbert Krebbers authored Jul 13, 2019
  
  06f3218d
- Merge branch 'ralf/pair-core' into 'master' · b91b45a1
  Robbert Krebbers authored Jul 13, 2019
```
show that pair construction commutes with taking the core

See merge request iris!286
```
  b91b45a1
- shorten proof · 9a04511b
  Ralf Jung authored Jul 13, 2019
  
  9a04511b
12 Jul, 2019 2 commits
- tweak proof to also work after a Coq bugfix · 927a2930
  Ralf Jung authored Jul 12, 2019
  
  927a2930
- changelog for comparison changes · 0dec8845
  Ralf Jung authored Jul 12, 2019
  
  0dec8845
09 Jul, 2019 4 commits
- dont quantify over empty telescopes · 3b2111d4
  Ralf Jung authored Jul 09, 2019
  
  3b2111d4
- Merge branch 'fresh_locs_arg' into 'master' · e1198994
  Robbert Krebbers authored Jul 09, 2019
```
Get rid of a superflous argument to `fresh_locs`.

See merge request iris!288
```
  e1198994
- Get rid of a superflous argument to `fresh_locs`. · 669ebceb
  Dan Frumin authored Jul 09, 2019
  
  669ebceb
- bump std++ · a649496c
  Ralf Jung authored Jul 09, 2019
  
  a649496c
07 Jul, 2019 1 commit
- show that pair cosntruction commutes with taking the core · c07a5eec
  Ralf Jung authored Jul 07, 2019
  
  c07a5eec
05 Jul, 2019 2 commits
- Bump stdpp. · 86da40a5
  Robbert Krebbers authored Jul 05, 2019
  
  86da40a5
- Add lemma `big_sepL2_reverse`. · 6a8e57e7
  Robbert Krebbers authored Jul 05, 2019
  
  6a8e57e7
03 Jul, 2019 4 commits
- Merge branch 'ralf/update' into 'master' · 69d22cfa
  Ralf Jung authored Jul 03, 2019
```
provide a lemma to update only the authoritative part, ignoring the fragments entirely

See merge request iris!284
```
  69d22cfa
- Stronger local update for multisets that entails the old ones. · de760be0
  Robbert Krebbers authored Jul 03, 2019
  
  de760be0
- Add lemmas for `≼` of `Cinl` and `Cinr`. · 1519c178
  Robbert Krebbers authored Jul 03, 2019
  
  1519c178
- provide a lemma to update only the authoritative part, ignoring the fragments entirely · 7365aa1c
  Ralf Jung authored Jul 03, 2019
  
  7365aa1c
01 Jul, 2019 4 commits
- Merge branch 'ralf/eq' into 'master' · 4e176be4
  Ralf Jung authored Jul 01, 2019
```
heap_lang: Make binary "=" operator partial, to sync with CmpXchg

Closes #248

See merge request iris!283
```
  4e176be4
- Make `iPure` non-local so it can be used for defining custom `iDestruct`-like tactics. · 56bd844b
  Robbert Krebbers authored Jul 01, 2019
  
  56bd844b
- use decide instead of bool_decide where possible · 79e6cf74
  Ralf Jung authored Jul 01, 2019
  
  79e6cf74
- minor tweaks · fcd36ce1
  Ralf Jung authored Jul 01, 2019
  
  fcd36ce1
30 Jun, 2019 2 commits
- bump std++ · bb7e98b1
  Ralf Jung authored Jun 30, 2019
  
  bb7e98b1
- Bump stdpp. · aa68f691
  Robbert Krebbers authored Jun 30, 2019
  
  aa68f691
29 Jun, 2019 1 commit

heap_lang: Make binary "=" operator partial, to sync with CmpXchg · 09b43741

Ralf Jung authored Jun 28, 2019

This also gets rid of [val_for_compare]-normalization; instead we introduce a
[LitErased] literal that is suited for use by erasure theorems.

09b43741

28 Jun, 2019 2 commits
- Bump std++. · 13f7e88b
  Robbert Krebbers authored Jun 29, 2019
  
  13f7e88b
- Up to 15 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`! · 676524b6
  Robbert Krebbers authored Jun 28, 2019
```
This commit made me cry...
```
  676524b6