section "Arithmetic and Boolean Expressions" subsection "Arithmetic Expressions" theory AExp imports Main begin type_synonym vname = string type_synonym val = int type_synonym state = "vname ⇒ val" text_raw‹\snip{AExpaexpdef}{2}{1}{%›