(* Variables *)
-inductive Var : Type[0] ≝
+ inductive Var : Type[0] ≝
Id : nat → Var.
(* Arithmetic expressions *)
.
interpretation "Aexp plus" 'plus x y = (Add x y).
-interpretation "Aexp minus" 'plus x y = (Sub x y).
+interpretation "Aexp minus" 'minus x y = (Sub x y).
interpretation "Aexp times" 'times x y = (Mul x y).
(* Boolean expressions *)