book/TPiL/StructuresAndRecords.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
  1. structure (structure at line 22) line 22 source
  2. instance of line 25 source

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

  3. inductive data line 44 source

    Distinct definitions of this name: book/TPiL/InductionAndRecursion.lean:295 (different declaration text). Qualify references as data@path.

  4. structure with.Point line 55 source
  5. structure with.Point line 63 source
  6. structure with.Point line 78 source
  7. structure with.Point line 108 source
  8. example with.(example at line 118) line 118 source
  9. example with.(example at line 121) line 121 source
  10. structure with.Point line 129 source
  11. structure with.Point line 142 source
  12. def with.p line 146 source

    Source comment

    ----
    def p := Point.mk 10 20
…
  13. structure with.Point line 163 source
  14. def with.Point.add line 168 source
  15. def with.p line 171 source
  16. def with.q line 172 source
  17. structure with.Point line 180 source
  18. structure with.Point line 201 source
  19. def with.Point.smul line 206 source

    Source comment

    ----
    def Point.smul (n : Nat) (p : Point Nat) :=
…

    Mentions: n, with.p, with.Point

  20. def with.p line 209 source
  21. example with.(example at line 213) line 213 source
  22. def with.xs line 223 source
  23. def with.f line 224 source
  24. example with.(example at line 228) line 228 source
  25. structure with.Point line 259 source
  26. example with.(example at line 269) line 269 source
  27. structure with.MyStruct line 281 source
  28. structure with.object line 294 source
  29. structure with.Point line 301 source
  30. def with.p line 306 source
  31. structure with.Point3 line 313 source
  32. def with.q line 318 source
  33. def with.r line 321 source
  34. example with.(example at line 324) line 324 source
  35. example with.(example at line 325) line 325 source
  36. example with.(example at line 326) line 326 source
  37. structure with.Point line 338 source
  38. inductive with.Color line 342 source
  39. structure with.ColorPoint line 345 source
  40. structure with.Point line 353 source
  41. structure with.RGBValue line 358 source
  42. structure with.RedGreenPoint line 363 source
  43. def with.p line 366 source
  44. def with.rgp line 369 source
  45. example with.(example at line 372) line 372 source
  46. example with.(example at line 373) line 373 source