HL Terse source diff

HL/Equiv.lean

480480   rw [TotalMap.update_eq, TotalMap.update_eq] at contra
481481   contradiction
482482 
483--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
483+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

HL/Hoare.lean

14781478 --  the rules of Hoare logic as a closed world for reasoning
14791479 --  about programs.
14801480 
1481--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1481+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

HL/Hoare2.lean

957957 --       while (true) {X := 0}
958958 --       {{ X = 0 }}
959959 
960--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
960+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

HL/Imp.lean

11451145 
11461146 end StackCompiler
11471147 
1148--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1148+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

HL/Preface.lean

8080 --  National Science Foundation under the NSF Expeditions
8181 --  grant 1521523, *The Science of Deep Specification*.
8282 
83--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
83+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

HL/Slang.lean

416416 --  Functional: computation. Relational: expressive. Best:
417417 --  both, proved equivalent.
418418 
419--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
419+-- 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

15491549 
15501550 end Reflection
15511551 
1552--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1552+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC