instance 検索の深さの上限を示す

instance のページに下記の例を追記したい

inductive Even : Type where
  | zero : Even
  | succ : Even → Even

def Even.toNat : Even → Nat
  | zero => 0
  | succ n => 2 + (Even.toNat n)

instance : ToString Even where
  toString := toString ∘ Even.toNat

instance : OfNat Even 0 where
  ofNat := Even.zero

#check (0 : Even)

instance [OfNat Even n] : OfNat Even (n + 2) where
  ofNat := Even.succ (OfNat.ofNat n)

#eval (2 : Even)

#check_failure (3 : Even)

#eval (254 : Even)

#check_failure (256 : Even)

lean-ja / lean-by-example

instance 検索の深さの上限を示す #406