SF-in-Lean previews

TS Terse source diff

Switch volume / audience

LF

StudentTerseTeacher (solutions)

HL

StudentTerseTeacher (solutions)

TS

StudentTerseTeacher (solutions)

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

TS/MoreStlc.lean

10181018 
10191019 end StlcExtended
10201020 
1021--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1021+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Preface.lean

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

TS/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

TS/Smallstep.lean

10491049 example : (.p (.c 3) (.p (.c 3) (.c 4))) ⟶* (.c 10) := by
10501050   normalize using SimpleArith
10511051 
1052--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1052+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Stlc.lean

12451245 
12461246 end Stlc
12471247 
1248--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1248+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/StlcProp.lean

621621 
622622 end StlcArith
623623 
624--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
624+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Sub.lean

12551255 
12561256 end StlcSub
12571257 
1258--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1258+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Types.lean

860860 --  Why might we prefer the small-step semantics for stating
861861 --  preservation and progress?
862862 
863--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
863+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS.lean

77 import TS.MoreStlc
88 import TS.Sub
99 
10--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
10+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC