search

leanprover / fp-lean

Functional Programming in Lean
Other
59 stars 15 forks source link

Ch 4.2 Even Number Literals exercise has an outdated hint #132

Open sanpoyur opened 9 months ago

sanpoyur commented 9 months ago

For the base instance, it is necessary to write OfNat Even Nat.zero instead of OfNat Even 0.

After https://github.com/leanprover/lean4/issues/1389 was closed, OfNat instances defined with Nat literals could be resolved directly, so this hint is outdated. I did this exercise using OfNat Even 0, and it works fine.

david-christiansen commented 8 months ago

Thanks! I'll investigate and follow up in my next batch of updates to the book.