LF Terse source diff
LF/Automation.lean
663663
664664 end RegExp
665665
666--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
666+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Basics.lean
979979
980980 end Nat
981981
982--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
982+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/IndProp.lean
716716 -- The characterizing lemmas for `∈` are called
717717 -- `List.mem_nil_iff` and `List.mem_cons`.
718718
719--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
719+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Induction.lean
445445 example (b c : Bool) : (b && c) = (c && b) := by
446446 cases b <;> cases c <;> rfl
447447
448--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
448+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Lists.lean
576576
577577 end Lists
578578
579--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
579+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Logic.lean
13391339 -- Output:
13401340 -- Classical.em (p : Prop) : p ∨ ¬p
13411341
1342--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1342+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Poly.lean
687687 -- Output:
688688 -- fold_plus : List Nat → Nat → Nat
689689
690--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
690+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Postscript.lean
6868 -- develops formalized mathematics using Lean and
6969 -- Mathlib.
7070
71--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
71+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Preface.lean
488488 -- National Science Foundation under the NSF Expeditions
489489 -- grant 1521523, *The Science of Deep Specification*.
490490
491--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
491+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Tactics.lean
722722 -- generalizing the listed local variables, giving a more
723723 -- general induction hypothesis
724724
725--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
725+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/Typeclasses.lean
15491549
15501550 end Reflection
15511551
1552--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
1552+-- Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC
LF/UsingLean.lean
268268 theorem Nat.double_zero : double 0 = 0 := by rfl
269269 theorem Nat.double_succ (n : Nat) : (n + 1).double = n.double + 2 := by rfl
270270
271--- Source revision: 958a218, committed 2026-09-28 10:35 UTC
271+-- 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