Commits · 9274f33d1c040e9b86383e769d86aa6d6a915d70 · Yixuan Chen / Iris

Jun 27, 2022
- normalize away new section variable info · 9274f33d
  Ralf Jung authored 2 years ago
  
  9274f33d
Jun 10, 2022
- docs for aupd_intro · 53b20974
  Ralf Jung authored 2 years ago
  
  53b20974
- Merge branch 'ralf/au-intro' into 'master' · d3bdb709
  Ralf Jung authored 2 years ago
  
  make iAuIntro smarter See merge request iris/iris!806
  d3bdb709
Jun 09, 2022
- add a test · fe43c8df
  Ralf Jung authored 2 years ago
  
  fe43c8df
- make iAuIntro smarter · 3e0e21a2
  Ralf Jung authored 2 years ago
  
  3e0e21a2
- Merge branch 'ralf/proofmode-of-envs' into 'master' · 01557046
  Ralf Jung authored 2 years ago
  
  adjust proofmode of_envs to rely less on persistently_emp_2 See merge request iris/iris!794
  01557046
- remove of_envs_eq'; add of_envs_alt · d3f9e01a
  Ralf Jung authored 2 years ago
  
  d3f9e01a
- changelog · f7840f2a
  Ralf Jung authored 2 years ago
  
  f7840f2a
- rename env_and_pers → env_and_persistently · f9b965cf
  Ralf Jung authored 2 years ago
  
  f9b965cf
- Use big op properly instead of `env_map`. Simplify some proofs. · 7fd2a308
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  7fd2a308
- document what needs to be in pm_eval · f02ecca3
  Ralf Jung authored 2 years ago
  
  f02ecca3
- adjust proofmode of_envs to rely less on persistently_emp_2 · 5f7e437f
  Ralf Jung authored 2 years ago
  
  5f7e437f
Jun 08, 2022
- Merge branch 'robbert/big_andL_absorbing' into 'master' · 39da88b3
  Ralf Jung authored 2 years ago
  
  Add `Absorbing` instances for `[∧ list]`. See merge request iris/iris!805
  39da88b3
- normalize away some trailing spaces · 62e50f6b
  Ralf Jung authored 2 years ago
  
  62e50f6b
- update dependencies · 16658674
  Ralf Jung authored 2 years ago
  
  16658674
- Add `Absorbing` instances for `[∧ list]`. · 23248949
  Robbert Krebbers authored 2 years ago
  
  23248949
Jun 07, 2022
- Merge branch 'functors' into 'master' · 50cb1b9d
  Ralf Jung authored 2 years ago
  
  Add some missing functors in algebra/lib See merge request iris/iris!803
  50cb1b9d
- Add some missing functors in algebra/lib · 4563868c
  Lennard Gäher authored 2 years ago and Ralf Jung committed 2 years ago
  
  4563868c
Jun 03, 2022
- Merge branch 'ralf/tex-heaplang' into 'master' · 7ad5d72c
  Ralf Jung authored 2 years ago
  
  document HeapLang syntax and operational semantics See merge request iris/iris!800
  7ad5d72c
May 25, 2022

Merge branch 'ralf/triples' into 'master' · d46e4472

Ralf Jung authored 2 years ago

fix triple issues with revert, and add logatom triples

See merge request iris/iris!801

d46e4472

May 24, 2022
- Merge branch 'atomic-flip' into 'master' · 5a3fc21a
  Ralf Jung authored 2 years ago
  
  Flip atomic updates quantifiers compared to atomic triples See merge request iris/iris!750
  5a3fc21a
- changelog · 08d1fac0
  Ralf Jung authored 2 years ago
  
  08d1fac0
- Flip quantifiers for atomic updates, and double them up · 5c1b38c5
  Paolo G. Giarrusso authored 3 years ago and Ralf Jung committed 2 years ago
  
  5c1b38c5
May 23, 2022
- add logically atomic triples · f8710e19
  Ralf Jung authored 2 years ago
  
  f8710e19
- Revert "Merge branch 'iris_style_improvements' into 'master'" · b60fbd73
  Ralf Jung authored 2 years ago
  
  This reverts commit bfb57e8b, reversing changes made to 56e9d264. Fixes the problem reported at <iris/iris!797 (comment 81110)>
  b60fbd73
- add a test document for our macros · 3e0fecca
  Ralf Jung authored 2 years ago
  
  3e0fecca
May 21, 2022
- (maybe) better symbol for Ptradd · f9181595
  Ralf Jung authored 2 years ago
  
  f9181595
- remove MatchCore macro, and add sugar for match with binders · 8dc969d0
  Ralf Jung authored 2 years ago
  
  8dc969d0
- add short-circuiting boolean operations · ee8476c4
  Ralf Jung authored 2 years ago
  
  ee8476c4
May 18, 2022
- document HeapLang syntax and operational semantics · 6676a195
  Ralf Jung authored 2 years ago
  
  6676a195
- Merge branch 'iris_style_improvements' into 'master' · bfb57e8b
  Ralf Jung authored 2 years ago
  
  Make Hoare triple tex macro compatible with e.g. array environment See merge request iris/iris!797
  bfb57e8b
May 17, 2022
- cleanup imports · 56e9d264
  Ralf Jung authored 2 years ago
  
  56e9d264
- Merge branch 'paolo/fix-461' into 'master' · 9dd4d1ea
  Ralf Jung authored 2 years ago
  
  Add testcase for #461 See merge request iris/iris!798
  9dd4d1ea
May 16, 2022
- bump std++ properly · 2ce5597c
  Ralf Jung authored 2 years ago
  
  2ce5597c
- bump std++ · 15e60f74
  Ralf Jung authored 2 years ago
  
  15e60f74
- Add testcase for #461 · 9851ef8d
  Paolo G. Giarrusso authored 2 years ago
  
  Verified
  
  9851ef8d
- Bump stdpp for universe fix · e60de03f
  Paolo G. Giarrusso authored 2 years ago
  
  Verified
  
  e60de03f
- use tc_opaque for a complicated definition · 1b5e1bc6
  Ralf Jung authored 2 years ago
  
  1b5e1bc6
- updates preserve being Absorbing · 15fd682e
  Ralf Jung authored 2 years ago
  
  15fd682e
- Renamed internal macro · c4857c8a
  Jonas Kastberg authored 2 years ago
  
  c4857c8a