LF Teacher (solutions) source diff
LF/Automation.lean
16791679
16801680 end PalConv
16811681
1682--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1682+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Basics.lean
15151515
15161516 def blt (n m : Nat) : Bool := (ble (succ n) m)
15171517
1518-example : blt two two = false := (by rfl)
1519-example : blt two four = true := (by rfl)
1518+theorem blt_test1 : blt two two = false := (by rfl)
1519+theorem blt_test2 : blt two four = true := (by rfl)
15201520 theorem blt_test3 : blt four two = false := (by rfl)
15211521
15221522 attribute [irreducible] blt ble
22702270 end Airport
22712271 end NatPlayground
22722272
2273--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
2273+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/IndProp.lean
23962396 Repeats l₁ :=
23972397 pigeonhole_aux l₁ [] l₂ hin hlen
23982398
2399--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
2399+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Induction.lean
11261126 end NatToBin
11271127 end NatPlayground.Nat
11281128
1129--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1129+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Lists.lean
13471347
13481348 end Lists
13491349
1350--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1350+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Logic.lean
23902390 theorem peirce_cm : Peirce → ConsequentiaMirabilis := by
23912391 intro h a; exact h a False
23922392
2393--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
2393+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Poly.lean
13991399
14001400 end Church
14011401
1402--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1402+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Postscript.lean
6363 -- Lean](https://leanprover-community.github.io/mathematics_in_lean/)
6464 -- develops formalized mathematics using Lean and Mathlib.
6565
66--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
66+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Preface.lean
419419 -- Note to developers (Benjamin Pierce @bcpierce00):
420420 -- Other funding should be acknowledged here...
421421
422--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
422+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Tactics.lean
15731573 rw [anyTrue, ih, anyTrue', anyTrue', allTrue]
15741574 rw [Bool.not_and, Bool.not_not]
15751575
1576--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1576+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Typeclasses.lean
16761676
16771677 end Reflection
16781678
1679--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1679+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/UsingLean.lean
526526 -- With these tools in hand, we can begin to prove properties about more
527527 -- sophisticated forms of data, beginning with `Lists`.
528528
529--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
529+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF.lean
1111 import LF.Typeclasses
1212 import LF.Postscript
1313
14--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
14+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC