Inductive op :=
  | Add

Inductive expr :=
  | Const int
  | BinOP op expr expr

eval : expr -> int
eval Const(i)         := i
eval BinOp(Add,e1,e2) := eval e1 + eval e2


compile Const(i)         := gen.Const(i)
compile BinOp(Add,e1,e2) := compile e1; compile e2; compile.Add


check Const(i)         := true
check BinOp(Add,e1,e2) := check e1 && check e2


main :=
  let p := (BinOp(Add, BinOp(Add, Const 5, Const 3), Const 2) in
  check p
  eval p
  compile p