Funcons-beta : Computation-Types.cbs | PRETTY | PDF
Computation Types
Built-in Funcon
computation-types : types
For any value type T
, the term =>T
is the type of computations that
compute values of type T
whenever they terminate normally.
For any subtypes S
, T
of values
, S=>T
is the type of computations
that compute values of type T
whenever they terminate normally, and
either do not refer at all to the given
entity, or require the given
entity to have type S
.