For §3.1.6.2 Even Numbers, I wrote Even as a structural type that just doubles a Nat, since the immediately prior exercise had me rewrite Pos that way. But then when I came to §3.2.4.1 and it told me to write an OfNat instance relying on recursive instance search, I couldn't find any way to do this. I tried searching online for this problem and found this StackExchange answer which demonstrates how to solve it with an inductive definition, and based on what it's saying there (that Lean needs to be able to syntactically manipulate the literal into the form n + 2) it sounds like there's just no way to get this to work with the structural definition as Lean cannot syntactically manipulate a literal into n * 2 (or if there is some alternative solution, then it requires more advanced knowledge).
Given the difficulty here, I think the §3.1.6.2 exercise really should ask me to define an inductive datatype.
For §3.1.6.2 Even Numbers, I wrote
Evenas a structural type that just doubles aNat, since the immediately prior exercise had me rewritePosthat way. But then when I came to §3.2.4.1 and it told me to write anOfNatinstance relying on recursive instance search, I couldn't find any way to do this. I tried searching online for this problem and found this StackExchange answer which demonstrates how to solve it with an inductive definition, and based on what it's saying there (that Lean needs to be able to syntactically manipulate the literal into the formn + 2) it sounds like there's just no way to get this to work with the structural definition as Lean cannot syntactically manipulate a literal inton * 2(or if there is some alternative solution, then it requires more advanced knowledge).Given the difficulty here, I think the §3.1.6.2 exercise really should ask me to define an inductive datatype.