module Exp3 where data Nat : Set where z : Nat s : Nat → Nat {-# BUILTIN NATURAL Nat #-} {-# BUILTIN ZERO z #-} {-# BUILTIN SUC s #-} _+_ : Nat → Nat → Nat z + n = n s m + n = s (m + n) data Bool : Set where tt : Bool ff : Bool if_then_else_ : {A : Set} → Bool → A → A → A if tt then x else y = x if ff then x else y = y data Exp : Set where Val : Nat → Exp Add : Exp → Exp → Exp Cond : Bool → Exp → Exp → Exp eval : Exp → Nat eval (Val n) = n eval (Add e1 e2) = eval e1 + eval e2 eval (Cond b e1 e2) = if b then eval e1 else eval e2