Commits · step-index-class · Iris / transfinite

Sep 11, 2022
- finish making step-index a typeclass · 9c36e6af
  Simon Spies authored 2 years ago
  
  9c36e6af
- add type class to bi · 1df456c6
  Simon Spies authored 2 years ago
  
  1df456c6
- fix the remainder of the algebra folder · a0260396
  Simon Spies authored 2 years ago
  
  a0260396
- index as type class · accf80a6
  Simon Spies authored 2 years ago
  
  accf80a6
Sep 10, 2022
- update files to match stdpp · 6844ee66
  Simon Spies authored 2 years ago
  
  6844ee66
Sep 09, 2022
- update files to new version · 1987fad2
  Simon Spies authored 2 years ago
  
  1987fad2
- outdated files from another version · 191bc121
  Simon Spies authored 2 years ago
  
  191bc121
- remove examples and instances · 792a63bc
  Simon Spies authored 2 years ago
  
  792a63bc
- remove old options file in algebra · e865f697
  Simon Spies authored 2 years ago
  
  e865f697
- new versions of the step-indexing files · 369dc242
  Simon Spies authored 2 years ago
  
  369dc242
- add iris prelude · 6f31e0eb
  Simon Spies authored 2 years ago
  
  6f31e0eb
- update coq project and opam · 7c06b30a
  Simon Spies authored 2 years ago
  
  7c06b30a
Apr 14, 2021
- update license · 0ad25f97
  Lennard Gäher authored 4 years ago
  
  0ad25f97
Dec 08, 2020
- gstep rule · 904f6c86
  Simon Spies authored 4 years ago
  
  904f6c86
Nov 28, 2020
- Update README.md · c2247c3a
  Lennard Gäher authored 4 years ago
  
  c2247c3a
Nov 24, 2020
- use non-timing runner · 4d112423
  Ralf Jung authored 4 years ago
  
  4d112423
- add CI back in · 52fe6ce9
  Lennard Gäher authored 4 years ago
  
  52fe6ce9
- rebase transfinite iris · 0c58544d
  Lennard Gäher authored 4 years ago
  
  0c58544d
Jul 22, 2019
- mention how to use iLöb for recursive functions · 75a18932
  Ralf Jung authored 5 years ago
  
  75a18932
Jul 14, 2019
- Merge branch 'big_sepL2_app_inv_2' into 'master' · e1d90815
  Robbert Krebbers authored 5 years ago
  
  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 5 years ago and Robbert Krebbers committed 5 years ago
  
  And shorten the proof.
  19e02ccc
- Merge branch 'head_prim_fill_reducible' into 'master' · ff179bf5
  Robbert Krebbers authored 5 years ago
  
  Add `head_prim_fill_reducible`. See merge request iris!293
  ff179bf5
- Add `head_prim_fill_reducible`. · 6e7d8b43
  Dan Frumin authored 5 years ago and Robbert Krebbers committed 5 years ago
  
  A more general implication from `head_reducible` to `reducible`.
  6e7d8b43
Jul 13, 2019
- Merge branch 'sigTO_proper_projs' into 'master' · f1cead30
  Robbert Krebbers authored 5 years ago
  
  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 5 years ago and Robbert Krebbers committed 5 years ago
  
  8c68ae86
- proper link and less Rust ;) · 49a876b6
  Ralf Jung authored 5 years ago
  
  49a876b6
- erasure is in iris/examples · 2663ac37
  Ralf Jung authored 5 years ago
  
  2663ac37
- Weaken premise of `gmultiset_local_update_dealloc`. · 06f3218d
  Robbert Krebbers authored 5 years ago
  
  06f3218d
- Merge branch 'ralf/pair-core' into 'master' · b91b45a1
  Robbert Krebbers authored 5 years ago
  
  show that pair construction commutes with taking the core See merge request iris!286
  b91b45a1
- shorten proof · 9a04511b
  Ralf Jung authored 5 years ago
  
  9a04511b
Jul 12, 2019
- tweak proof to also work after a Coq bugfix · 927a2930
  Ralf Jung authored 5 years ago
  
  927a2930
- changelog for comparison changes · 0dec8845
  Ralf Jung authored 5 years ago
  
  0dec8845
Jul 09, 2019
- dont quantify over empty telescopes · 3b2111d4
  Ralf Jung authored 5 years ago
  
  3b2111d4
- Merge branch 'fresh_locs_arg' into 'master' · e1198994
  Robbert Krebbers authored 5 years ago
  
  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 5 years ago
  
  669ebceb
- bump std++ · a649496c
  Ralf Jung authored 5 years ago
  
  a649496c
Jul 07, 2019
- show that pair cosntruction commutes with taking the core · c07a5eec
  Ralf Jung authored 5 years ago
  
  c07a5eec
Jul 05, 2019
- Bump stdpp. · 86da40a5
  Robbert Krebbers authored 5 years ago
  
  86da40a5
- Add lemma `big_sepL2_reverse`. · 6a8e57e7
  Robbert Krebbers authored 5 years ago
  
  6a8e57e7
Jul 03, 2019

Merge branch 'ralf/update' into 'master' · 69d22cfa

Ralf Jung authored 5 years ago

provide a lemma to update only the authoritative part, ignoring the fragments entirely

See merge request iris!284

69d22cfa