Typed 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 T ::= Bool Nat Typing Rules TODO Evaluation Rules TODO