I'm working my way through Functional Programming in Lean. There's an exercise to create an
Even class to represent even natural numbers.
I was able to define addition, multiplication, and
toNat, but defining using recursive instance search to define
Even has me stumped. Here's my basic scaffolding for
inductive Even : Type where | zero | succ : Even → Even def Even.toNat : Even → Nat | Even.zero => 0 | Even.succ n => 2 + n.toNat instance : ToString Even where toString n := toString n.toNat
OfNat, I have the base case figured out:
instance : OfNat Even 0 where ofNat := Even.zero def zeroEven : Even := 0
The book says I need
0 worked just fine.
My code for the recursive case does not compile; it's my best guess so far, but the book has not taught
inferInstance yet, so there's probably a simpler solution that doesn't use it:
instance : OfNat Even (n + 2) where ofNat := Even.succ (inferInstance : OfNat Even n).ofNat
The error message is on
inferInstance and says
failed to synthesize instance OfNat Even n. I believe the basic idea is right, though; I need to synthesize an
n+2 by taking the successor of a synthesized
n, and so on with
0 as the base case.
What am I doing wrong? How do I synthesize
Even via recursive instance search?