Example. Definitions, Datatypes, Induction, Functions › The oot type [isa-001J]
This defines a type called oot with two values, ONE : oot and TWO : oot. The print_theorems command here allows us to see all of the theorems automatically created by the datatype command, chiefly that the constants ONE and TWO are disjoint (i.e. ONE ≠ TWO) and exhaustive (i.e. that there are no other values of type oot apart from ONE and TWO)