HL Student source diff
HL/Equiv.lean
16051605 theorem zprop_preserving (c c' : Com) (hc : zprop c) (ha : Approx c c') : zprop c' := by
16061606 sorry
16071607
1608--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1608+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC
HL/Hoare.lean
27312731
27322732 end HoareAssertAssume
27332733
2734--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
2734+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC
HL/Hoare2.lean
19441944
19451945 end HimpHoare2
19461946
1947--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1947+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC
HL/Imp.lean
15731573 -- Notation for `for` loops, but feel free to play with this too if you
15741574 -- like.)
15751575
1576--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1576+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC
HL/Preface.lean
6868 -- was supported, in part, by the National Science Foundation under the
6969 -- NSF Expeditions grant 1521523, *The Science of Deep Specification*.
7070
71--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
71+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC
HL/Slang.lean
614614 -- switch between points of view at will -- exactly what we did above in
615615 -- `Slang.Aexp.evalR_iff_eval` and `Slang.Bexp.evalR_iff_eval`.
616616
617--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
617+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC
HL.lean
55 import HL.Hoare
66 import HL.Hoare2
77
8--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
8+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC
LF/Typeclasses.lean
16551655
16561656 end Reflection
16571657
1658--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1658+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC