fix(induction_and_recursion): typo

leanprover / theorem_proving_in_lean

Theorem proving in Lean

Apache License 2.0

47 stars 46 forks source link

Closed pechersky closed 4 years ago

pechersky commented 4 years ago

fix(induction_and_recursion): typo

Change example of inaccessible terms to work with lean 3.11.0 and later. In 3.11.0, previous syntax is wrong due to new rules about implicit-ness of constructors. Fixes identified by Bryan Gin-ge Chen and Reid Barton in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Inaccessible.20terms.20and.20non-working.20TPIL.20example/near/199825461.

avigad commented 4 years ago

I'm sorry I missed this when it was first posted. I'll merge now.