HL Teacher (solutions) source diff

HL/Equiv.lean

20342034   obtain ⟨st', h⟩ := hc
20352035   apply ha at h; exists st'
20362036 
2037--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
2037+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

HL/Hoare.lean

34503450 
34513451 end HoareAssertAssume
34523452 
3453--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
3453+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

HL/Hoare2.lean

30153015 
30163016 end HimpHoare2
30173017 
3018--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
3018+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

HL/Imp.lean

19241924 --  Notation for `for` loops, but feel free to play with this too if you
19251925 --  like.)
19261926 
1927--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1927+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

HL/Preface.lean

7171 --  Note to developers (Benjamin Pierce @bcpierce00):
7272 --      Other funding should be acknowledged here...
7373 
74--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
74+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

HL/Slang.lean

681681 --  switch between points of view at will -- exactly what we did above in
682682 --  `Slang.Aexp.evalR_iff_eval` and `Slang.Bexp.evalR_iff_eval`.
683683 
684--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
684+-- 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

17121712 
17131713 end Reflection
17141714 
1715--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1715+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC