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: 958a218, committed 2026-09-28 10:35 UTC
1608+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC

HL/Hoare.lean

27312731 
27322732 end HoareAssertAssume
27332733 
2734--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
2734+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC

HL/Hoare2.lean

19441944 
19451945 end HimpHoare2
19461946 
1947--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1947+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 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: 958a218, committed 2026-09-28 10:35 UTC
1576+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 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: 958a218, committed 2026-09-28 10:35 UTC
71+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 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: 958a218, committed 2026-09-28 10:35 UTC
617+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC

HL.lean

55 import HL.Hoare
66 import HL.Hoare2
77 
8--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
8+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC

LF/Typeclasses.lean

16551655 
16561656 end Reflection
16571657 
1658--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1658+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC