Language Reference This section contains the specification of the Arend language. Toggle Menu Lexical structure Definitions Modules Parameters Functions Type synonyms Data Higher inductive types Records Classes Meta definitions Coercion Level Expressions Goals Universes Pi types Sigma types Let Case Class extensions Box Prelude