Learning path

Each declaration appears after its prerequisites.

  1. Hidden.UProd.mem_swap auxiliary lemma for proving mem_respects
  2. whatever Avoid warnings
  3. five Example that fails: a numeral at a type that merely unfolds to Nat
  4. TPiL.exampleSubversoRev The SubVerso revision recorded in the example project's Lake manifest
  5. TPiL.extractFile Extracts the highlighted contents of an example
  6. TPiL.allInfo Extracts all messages from the given code
  7. TPiL.trailingText Splits the trailing text off some code
  8. TPiL.messageComment? Splits the marker that introduces a message off a comment's text, along with the severity it names, if any
  9. TPiL.ExpectedMessage A comment that describes the message a command produces
  10. TPiL.commentContents Extracts the text of a comment, which may span several lines
  11. TPiL.expectedComment The comment that describes a message
  12. TPiL.messageSeverityName The name of a message's severity
  13. TPiL.lastLineIndent The indentation of the last line of some code
  14. TPiL.trailingComment Extracts a trailing comment from code, if present
  15. TPiL.commentColumn The column at which the comment on a line begins, if it has one
  16. TPiL.isMessageCommentLine Whether a line is a comment that introduces a message
  17. TPiL.isCommentLine Whether a line consists of a comment, along with any surrounding whitespace
  18. TPiL.fixupAnchorComments Leading anchor comments are always incorrect
  19. TPiL.logCommentMismatch Reports a comment that doesn't describe the message its command produced
  20. TPiL.checkSeverity Reports a comment that names a severity other than the one its command produced
  21. TPiL.leanFirst Elaborates Lean blocks first, maintaining the order of blocks
  22. TPiL.suggest Internal detail of suggestion mechanism
  23. Weekday.next_previous next undoes previous, by cases on the constructors
  24. Weekday.Weekday.add_comm First attempt at commutativity of Nat addition (contains sorry)
  25. f' Alternative syntax:
  26. foo@book/TPiL/InteractingWithLean.lean a user-defined function
  27. {lit}`Nat`.Ex2.id2 In this example, implicit lambda introduction has been disabled because we use @ before {kw}fun
  28. {lit}`Nat`.Ex2.id5 In this example, implicit lambda introduction has been disabled because we used the binder annotation {...}
  29. and_commut An axiom: and is commutative, in a toy proof system
  30. modus_ponens Modus ponens as an inference rule on Proof
  31. ex Everything follows from false
  32. divides_trans Divisibility is transitive, so calc can chain it
  33. swap_pair Tactics can define data: swapping a pair
  34. swap_sum Swapping the two sides of a sum type