leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 47 forks source link

Typos in well-founded induction section #41

Closed abentkamp closed 6 years ago

abentkamp commented 6 years ago

Hi, I found these typos while going through the tutorial: Replace ∀ y, r y x → acc y by ∀ y, r y x → acc r y Replace ∀ y ≺ x, C x by ∀ y ≺ x, C y