SF-in-Lean previews

TS Teacher (solutions) source diff

Switch volume / audience

LF

StudentTerseTeacher (solutions)

HL

StudentTerseTeacher (solutions)

TS

StudentTerseTeacher (solutions)

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

TS/MoreStlc.lean

23442344 
23452345 end StlcExtended
23462346 
2347--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
2347+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Preface.lean

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

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

TS/Smallstep.lean

15831583   · normalize using SimpleArith
15841584   · constructor
15851585 
1586--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1586+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Stlc.lean

14501450 
14511451 end Stlc
14521452 
1453--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1453+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/StlcProp.lean

20112011 
20122012 end StlcArith
20132013 
2014--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
2014+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Sub.lean

23852385 
23862386 end StlcSub
23872387 
2388--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
2388+-- Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC

TS/Types.lean

12581258 --      throughout (and maybe in Smallstep and Imp?)... `dev` block headers
12591259 --      too, if we want to be really consistent.
12601260 
1261--- Source revision: dcf4433, committed 2026-09-24 17:39 UTC
1261+-- 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