### Datatypes
[ Type datatype-values Funcon datatype-value Funcon datatype-value-id Funcon datatype-value-elements ]
*/ Built-in Type datatype-values Built-in Funcon datatype-value(_:identifiers, _:values*) : datatype-values Funcon datatype-value-id(_:datatype-values) : =>identifiers
Ruledatatype-value-id(datatype-value(I:identifiers, _*:values*)) ~> I
Funcon datatype-value-elements(_:datatype-values) : =>values*
Ruledatatype-value-elements(datatype-value(_:identifiers, V*:values*)) ~> V*
/*A datatype value consists of an identifier and a sequence of values. 'Datatype T ::= ...' declares the type `T` to refer to a fresh value constructor in `types`, and asserts ``T <: datatype-values``. Each constructor funcon 'F(_:T1,...,_:Tn)' of the datatype declaration generates values in `T` of the form `datatype-value("F", V1, ..., Vn)` from `V1:T1`, ..., `Vn:Tn`. Note that a computation `X` cannot be directly included in datatype values: it is necessary to encapsulate it in `abstraction(X)`. 'Datatype T', followed by declarations of constructor funcons for 'T', allows specification of GADTs.