LF Student source diff
LF/Automation.lean
11781178 --
11791179 -- ∀ l, l = l.reverse → Pal l
11801180
1181--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1181+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Basics.lean
14811481
14821482 def blt (n m : Nat) : Bool := sorry
14831483
1484-example : blt two two = false := sorry
1485-example : blt two four = true := sorry
1484+theorem blt_test1 : blt two two = false := sorry
1485+theorem blt_test2 : blt two four = true := sorry
14861486 theorem blt_test3 : blt four two = false := sorry
14871487
14881488 attribute [irreducible] blt ble
21082108 end Airport
21092109 end NatPlayground
21102110
2111--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
2111+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/IndProp.lean
15681568 Repeats l₁ := by
15691569 sorry
15701570
1571--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1571+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Induction.lean
941941 end NatToBin
942942 end NatPlayground.Nat
943943
944--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
944+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Lists.lean
12321232
12331233 end Lists
12341234
1235--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1235+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Logic.lean
20252025 theorem peirce_cm : Peirce → ConsequentiaMirabilis := by
20262026 sorry
20272027
2028--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
2028+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Poly.lean
12791279
12801280 end Church
12811281
1282--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1282+-- 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
407407 -- was supported, in part, by the National Science Foundation under the
408408 -- NSF Expeditions grant 1521523, *The Science of Deep Specification*.
409409
410--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
410+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Tactics.lean
12851285 anyTrue test l = anyTrue' test l := by
12861286 sorry
12871287
1288--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1288+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Typeclasses.lean
14581458
14591459 end Reflection
14601460
1461--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1461+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/UsingLean.lean
509509 -- With these tools in hand, we can begin to prove properties about more
510510 -- sophisticated forms of data, beginning with `Lists`.
511511
512--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
512+-- 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