book/TPiL/DependentTypeTheory.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned Theorem Proving in Lean documentation, Pinned Theorem Proving in Lean 4 book index

85 declarations, 0 contain sorry, 1 declared as axioms

Imports (2)
  1. def m line 40 source
  2. def n line 41 source
  3. def b1 line 42 source
  4. def b2 line 43 source
  5. example (example at line 148) line 148 source
  6. def α line 203 source
  7. def β line 204 source
  8. def F line 205 source
  9. def G line 206 source
  10. def α line 220 source
  11. def β line 221 source
  12. def α line 235 source
  13. def F line 346 source
  14. def F line 355 source
  15. def f line 416 source

    Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:340 (different declaration text), book/TPiL/InductionAndRecursion.lean:833 (different declaration text), book/TPiL/InteractingWithLean.lean:468 (different declaration text), book/TPiL/Tactics.lean:1457 (different declaration text). Qualify references as f@path.

  16. def g line 417 source

    Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:341 (different declaration text), book/TPiL/Tactics.lean:1781 (different declaration text). Qualify references as g@path.

  17. axiom whatever Avoid warnings line 457 source

    Source comment

    Avoid warnings
    axiom whatever : α

    Mentions: α

  18. def b line 458 source
  19. example (example at line 464) line 464 source
  20. def f line 488 source

    Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:340 (different declaration text), book/TPiL/InductionAndRecursion.lean:833 (different declaration text), book/TPiL/InteractingWithLean.lean:468 (different declaration text), book/TPiL/Tactics.lean:1457 (different declaration text). Qualify references as f@path.

  21. def g line 489 source

    Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:341 (different declaration text), book/TPiL/Tactics.lean:1781 (different declaration text). Qualify references as g@path.

  22. opaque to line 526 source

    Distinct definitions of this name: book/TPiL/Tactics.lean:875 (different declaration text). Qualify references as to@path.

  23. def double line 547 source

    Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:150 (different declaration text). Qualify references as double@path.

  24. def double line 558 source

    Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:150 (different declaration text). Qualify references as double@path.

  25. def double line 568 source

    Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:150 (different declaration text). Qualify references as double@path.

  26. def double line 578 source

    Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:150 (same statement text; different proof or body). Qualify references as double@path.

  27. def pi line 593 source
  28. def add line 600 source

    Distinct definitions of this name: book/TPiL/InductionAndRecursion.lean:505 (different declaration text), book/TPiL/InteractingWithLean.lean:231 (different declaration text). Qualify references as add@path.

  29. def double line 609 source

    Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:150 (different declaration text). Qualify references as double@path.

  30. def add line 612 source

    Source comment

    ---

    Distinct definitions of this name: book/TPiL/InductionAndRecursion.lean:505 (different declaration text), book/TPiL/InteractingWithLean.lean:231 (different declaration text). Qualify references as add@path.

    def add (x : Nat) (y : Nat) :=
…

    Mentions: x

  31. def greater line 624 source
  32. def double line 636 source

    Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:150 (different declaration text). Qualify references as double@path.

  33. def doTwice line 639 source

    Source comment

    ---
    def doTwice (f : Nat → Nat) (x : Nat) : Nat :=
…

    Mentions: x

  34. def compose line 649 source
  35. def compose line 672 source
  36. def double line 674 source

    Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:150 (different declaration text). Qualify references as double@path.

  37. def square line 677 source

    Source comment

    ---
    def square (x : Nat) : Nat :=
…

    Mentions: x

  38. def Natural line 687 source
  39. def Natural line 691 source
  40. def five Example that fails: a numeral at a type that merely unfolds to Nat line 693 source

    Source comment

    ----

    L4DEL explanation

    def Natural := Nat makes Natural a new name, but numeral literals still need an OfNat Natural 5 instance that does not exist.

    1. The book defines Natural as an alternative name for Nat with def Natural := Nat.
    2. This code block is marked as an expected error: def five : Natural := 5 does not elaborate.
    3. The recorded message says Lean failed to synthesize an instance of OfNat Natural 5, because numerals are polymorphic and the expected type is Natural.
    4. The point is that Lean treats a defined name as equal to its unfolding, but not every name is unfolded in every context, such as instance lookup.

    Sources and attribution: Pinned Lean source (4e28129fdd58)

    def five : Natural := 5
…

    Mentions: Natural

  41. def twice_double line 727 source
  42. def twice_double line 735 source
  43. def t line 754 source
  44. def foo line 779 source

    Distinct definitions of this name: book/TPiL/InductionAndRecursion.lean:115 (different declaration text), book/TPiL/InteractingWithLean.lean:784 (different declaration text). Qualify references as foo@path.

  45. def compose line 795 source
  46. def doTwice line 798 source
  47. def doThrice line 801 source
  48. def compose line 811 source
  49. def doTwice line 814 source
  50. def doThrice line 817 source
  51. def compose line 826 source
  52. def doTwice line 827 source
  53. def doThrice line 828 source
  54. def cons line 1020 source
  55. def cons line 1046 source
  56. example (example at line 1076) line 1076 source
  57. def f line 1112 source

    Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:340 (different declaration text), book/TPiL/InductionAndRecursion.lean:833 (different declaration text), book/TPiL/InteractingWithLean.lean:468 (different declaration text), book/TPiL/Tactics.lean:1457 (different declaration text). Qualify references as f@path.

  58. def g line 1115 source

    Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:341 (different declaration text), book/TPiL/Tactics.lean:1781 (different declaration text). Qualify references as g@path.

  59. def h1 line 1118 source
  60. def h2 line 1123 source
  61. def Lst line 1140 source
  62. def Lst.cons line 1141 source
  63. def Lst.nil line 1142 source
  64. def Lst.append line 1143 source
  65. def Lst line 1155 source
  66. def Lst.cons line 1156 source
  67. def Lst.nil line 1157 source
  68. def Lst.append line 1158 source
  69. def as line 1162 source
  70. def bs line 1163 source
  71. def Lst line 1169 source
  72. def Lst line 1190 source
  73. def Lst.cons line 1191 source
  74. def Lst.nil line 1192 source
  75. def Lst.append line 1193 source
  76. def as line 1201 source
  77. def bs line 1202 source
  78. def Lst line 1215 source
  79. def Lst.cons line 1217 source
  80. def Lst.nil line 1218 source
  81. def Lst.append line 1219 source
  82. def as line 1223 source
  83. def bs line 1224 source
  84. def ident line 1235 source
  85. def ident line 1241 source