inductive Expr
| Var : UInt32 → Expr
| Val : UInt32 → Expr
| Add : Expr → Expr → Expr

open Expr

def dec (n : UInt32) : UInt32 :=
if n = 0 then 0 else n-1

def mkExpr : UInt32 → UInt32 → Expr | n, v =>
if n = 0 then Val v
else Add (mkExpr (n-1) (v+1)) (mkExpr (n-1) (dec v))

def eval : Expr → UInt32
| Var x   => 0
| Val v   => v
| Add l r   => eval l + eval r

def main : IO UInt32 :=
IO.println (toString $ eval (mkExpr 26 1)) *>
pure 0