|
|
|---|
|
|
|
|---|
Fixtype of Syntheto types.
This is a tagged union type, introduced by fty::deftagsum.
There are primitive types for booleans (the usual two), characters (ISO 8851-1, 8-bit, as in ACL2), strings (of the above characters, any length), and integers (all of them, unbounded.
There are collection types for finite sets of elements of another type, finite sequences of elements of another type, and finite maps with another type as domain and another type as range. These are like built-in polymorphic types.
There is an option type, which consists of the values of a base type plus an additional distinct value. This is like a built-in polymorphic sum type.
There are types with explicit definitions, which are referenced by name. Note that the primitive and collection types have implicit definitions. The actual explicit type definitions are formalized elsewhere in the abstract syntax.
Here we capture the types, as syntactic entities, that can be used, for instance, as types of variables. There are other syntactic types, such as product types, that can only be used to define types; these are defined elsewhere in the abstract syntax.