Untyped Arithmetic Expressions Syntax Terms t ::= true false if t then t else t 0 succ t pred t iszero t Values v ::= true false nv nv ::= 0 succ nv Evaluation Rules TODO