|
|
|---|
|
|
|
|---|
Fixtype of Leo types.
This is a tagged union type, introduced by fty::deftagsum.
These are the primitive types, identifiers (used as types), and the tuple types.
Tuple types have two or more components, but we do not require that here. We can formulate and prove that invariant separately. Keeping the abstract syntax of types more general also facilitates a possible future extension of Leo in which tuple types with one component are actually allowed.
Instead of a zero-element tuple type, we have a primitive unit type.