SF-in-Lean previews

TS Student source diff

Switch volume / audience

LF

StudentTerseTeacher (solutions)

HL

StudentTerseTeacher (solutions)

TS

StudentTerseTeacher (solutions)

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

TS/MoreStlc.lean

21602160 
21612161 end StlcExtended
21622162 
2163--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
2163+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Preface.lean

6969 --  was supported, in part, by the National Science Foundation under the
7070 --  NSF Expeditions grant 1521523, *The Science of Deep Specification*.
7171 
72--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
72+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

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

TS/Smallstep.lean

13511351 theorem normalize_ex : exists e', (.p (.c 3) (.p (.c 2) (.c 1))) ⟶* e' ∧ IsValue e' := by
13521352   sorry
13531353 
1354--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1354+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Stlc.lean

13611361 
13621362 end Stlc
13631363 
1364--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1364+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/StlcProp.lean

13121312 
13131313 end StlcArith
13141314 
1315--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1315+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Sub.lean

19361936 
19371937 end StlcSub
19381938 
1939--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1939+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Types.lean

931931 --  for nonterminating programs? Why might we prefer the small-step
932932 --  semantics for stating preservation and progress?
933933 
934--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
934+-- 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