The datatype command [isa-001K]

The datatype defines a new type (like typedecl) but also defines some special constants, called constructors, which make values of that type. Constructors may optionally take arguments, and these data types may be recursive.

datatype type_name = Constructor1 "arg_type1" "arg_type2" (* ... *) | Constructor2 (* ... *) (* ... *)

These datatypes are analogous to the algebraic data types found in many functional programming languages.

The datatype command automatically proves many lemmas about these types for you, chiefly:

• Disjointness: Values made with one constructor are not equal to values made with another constructor.
• Exhaustivity: The only values of this type are those made by the listed constructors.
• Injectivity: Two values of the same constructor are equal iff their arguments are equal.