TODO

  * more on-paper homework questions (e.g. for operational semantics)

  * for chapters 1 and 2, more and better examples? esp. for type derivation
    trees

  * copyright notices?

  * get rid of two lingering `cases` for `cases'` in `love09*demo.lean`

  * use nlinarith instead of arith?

Course

  Ask questions?

    * lecture 1: what is diff between a definition and an axiom?
    * lecture 2: what is the difference between a forward and a backward proof?
    * lecture 3: what is the point of derivation rules? or what is the type of ->?
    * lecture 4: what is the difference between induction and recursion? (Curry-Howard)
    * lecture 5: how would you define xor as an inductive predicate?
    * lecture 6: why do we care about the monad laws?
    * lecture 7: what is the difference between a standard Lean function and
      a metafunction?
    * lecture 8: what would be the benefits of having a deep encoding of
      arithmetic and Boolean expressions? (e.g. optimizer; side effects in
      expressions, e.g. function calls)
    * lecture 9: what is the point of Hoare logic? of VCGs? (Hoare logic =
      symbolic, induction-free); VCGs = take care of the Hoare logic bureaucracy
    * lecture 10: why bother with monotone functions, complete lattices,
      fixpoints?
    * lecture 11: what is the difference between a subtype and a quotient type?
      (actual student's question one year)
    * lecture 12: what are the advantages and disadvantages of implicit
      coercions?


TODO HOMEWORK 2023

  * `love04*homework.lean`: in question 2.1, if people use `induction'`
    instead of pattern matching + recursion, they get occurrences of
    `nat.succ` in the goal. To apply relevant lemmas to these goals, we have
    to use `nat.succ_eq_add_one` to rewrite `nat.succ m` into `m + 1`. We
    should tell people about this lemma (it currently first appears in demo
    05) or add it to the default simp set.

  * avoid {} in homework 6

  * Reference to love08_operational_semantics_exercise_sheet from homework 9
    does not work for students who haven't done the exercise!

  * Typo: "bounus" -> "bonus"

  * Avoid linarith in homework 4 (or give hint!)

  * Homework 4, question 2's subquestions are mislabeled, and 3.2 and 3.3 are
    about ℤ3, not ℝ3

  * homework 09 ex. 1.1: the proofs for `consequence`, `assign_intro` and
    `seq_intro` are exactly the same as those from the demo. Intentional?
    If so, maybe add a note so students aren't confused.

  * homework 10 ex. 2.2: Lean warns if this definition is marked noncomputable
    even though it doesn't have to be. Maybe add a note that this warning is
    expected and harmless.

  * Homework 2, remove duplicate question 2.3

  * `love06*homework.lean`: in question 1.2, `simp[map]` suffices. This is
    because mathlib puts the lemmas from `is_lawful_monad` into the global
    simp set.

  * homework 11 ex. 2.1 (bonus): Maybe add a hint along the lines of

      Remember that when defining a function f : N -> X for an input n : N,
      you can recurse on m if you have a hypothesis h : n < m in the context.

    I don't know if you mentioned this anywhere except the optional ex. 2.6 in
    hw 09, but it took me 5min of looking at the solution to remember that Lean
    accepts this sort of implicit termination argument.

  * avoid rw [...] syntax in solutions

