Commits · aac70c879ecdd001de2a82a5a18b1767f88f60a8 · Yixuan Chen / Iris

Jul 20, 2022
- Merge branch 'mono_nat_lb_own_0' into 'master' · aac70c87
  Ralf Jung authored 2 years ago
  
  add mono_nat_lb_own_0 See merge request iris/iris!817
  aac70c87
- Merge branch 'ralf/fixpoint-persistent' into 'master' · 8d186d37
  Robbert Krebbers authored 2 years ago
  
  general lemma that a fixpoint is Persistent/Absorbing/Affine See merge request !810
  8d186d37
Jul 19, 2022
- Merge branch 'discardable-savedprop' into 'master' · c0373603
  Ralf Jung authored 2 years ago
  
  Make saved props have discardable fractions See merge request !802
  c0373603
- Make saved props have discardable fractions · c4399239
  Lennard Gäher authored 2 years ago and Ralf Jung committed 2 years ago
  
  c4399239
- add lemams for validity of the 1 fraction · 8e5241da
  Ralf Jung authored 2 years ago
  
  8e5241da
- Merge branch 'robbert/lc_proofmode_fix' into 'master' · 4e25dc9b
  Ralf Jung authored 2 years ago
  
  Tweak priority of proof mode instances for £. Closes #470 See merge request iris/iris!818
  4e25dc9b
- changelog · 449ced9b
  Ralf Jung authored 2 years ago
  
  449ced9b
- Apply 2 suggestion(s) to 1 file(s) · 2056ec6f
  Ralf Jung authored 2 years ago
  
  2056ec6f
- Add lemmas for affine/absorbing/and strong variants for persistent. · c5d09720
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  c5d09720
- general lemma that a fixpoint is Persistent · a52b29fc
  Ralf Jung authored 2 years ago
  
  a52b29fc
Jul 18, 2022
- Add comment. · 6c174ea1
  Robbert Krebbers authored 2 years ago
  
  6c174ea1
- Add tests. · 8e1e9c03
  Robbert Krebbers authored 2 years ago
  
  8e1e9c03
Jul 16, 2022
- Tweak priority of proof mode instances for £. · 610ed564
  Robbert Krebbers authored 2 years ago
  
  This closes issue #470.
  610ed564
Jul 15, 2022
- add mono_nat_lb_own_0 · c6e56bd3
  Ralf Jung authored 2 years ago
  
  c6e56bd3
- add a test that uses heap_total · 2f866db4
  Ralf Jung authored 2 years ago
  
  2f866db4
Jul 14, 2022
- Merge branch 'lc-fupd-gen-refactor' into 'master' · 6c5d84e1
  Ralf Jung authored 2 years ago
  
  Fupd soundness lemmas always generate credits See merge request iris/iris!815
  6c5d84e1
- Fupd soundness lemmas always generate credits · 584702fd
  Lennard Gäher authored 2 years ago and Ralf Jung committed 2 years ago
  
  584702fd
Jul 13, 2022
- Merge branch 'ralf/smart-apply' into 'master' · 051c25c9
  Ralf Jung authored 2 years ago
  
  document wp_smart_apply See merge request iris/iris!811
  051c25c9
- clarify · 1c105c7d
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  1c105c7d
- Fix some very long lines. · 297fa447
  Robbert Krebbers authored 2 years ago
  
  297fa447
Jul 12, 2022
- support fractional framing of ghost_var (like mapsto) · 5634e2a8
  Ralf Jung authored 2 years ago
  
  5634e2a8
Jul 08, 2022
- Merge branch 'ralf/le-upd-proofmode' into 'master' · a513639d
  Ralf Jung authored 2 years ago
  
  add proofmode instances for le_upd See merge request iris/iris!813
  a513639d
- make an internal lemma local · 7db70704
  Ralf Jung authored 2 years ago
  
  7db70704
Jul 07, 2022
- add proofmode instances for le_upd · 57d390bb
  Ralf Jung authored 2 years ago
  
  57d390bb
- Merge branch 'ralf/leupd' into 'master' · ee671e0a
  Ralf Jung authored 2 years ago
  
  fix le_upd notation See merge request iris/iris!812
  ee671e0a
- fix le_upd notation · 151faf22
  Ralf Jung authored 2 years ago
  
  151faf22
- make a proof script slightly more robust · 11bb8eb2
  Ralf Jung authored 2 years ago
  
  11bb8eb2
- update dependencies · 1d312d31
  Ralf Jung authored 2 years ago
  
  1d312d31
- document wp_smart_apply · 1db4c77d
  Ralf Jung authored 2 years ago
  
  1db4c77d
Jul 05, 2022
- Merge branch 'iris-later-credits' into 'master' · a32f36a9
  Ralf Jung authored 2 years ago
  
  First Steps for Later Credits See merge request iris/iris!792
  a32f36a9
- First Steps for Later Credits · 7032de0e
  Simon Spies authored 2 years ago and Ralf Jung committed 2 years ago
  
  7032de0e
- add test user of proofoutlines · e399bd08
  Ralf Jung authored 2 years ago
  
  e399bd08
- update pftools.sty from my thesis · 8d81002c
  Ralf Jung authored 2 years ago
  
  not really a fully compatible replacement. we should really have an example use of this somewhere here...
  8d81002c
Jun 28, 2022
- update dependencies · b337ca8c
  Ralf Jung authored 2 years ago
  
  b337ca8c
Jun 27, 2022
- update dependencies · fd103ad0
  Ralf Jung authored 2 years ago
  
  fd103ad0
- Revert "normalize away new section variable info" · 220d7062
  Ralf Jung authored 2 years ago
  
  This partially reverts commit 9274f33d. The pattern is bogus, it blocks other patterns from running after empty lines.
  220d7062
- 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 !806
  d3bdb709
Jun 09, 2022
- add a test · fe43c8df
  Ralf Jung authored 2 years ago
  
  fe43c8df