10.2.2 Negative Types
This requires advanced features discussed in TBoS. Something belongs to the type (not number) if it
cannot be proved to be of the type number.
(datatype not
X : A; !; fail!;
_____________________
X : (mode (not A) -);
_____________________
X : (mode (not A) -);)
type#my-prover-types
f : (not number)
f : (not number)
f : (not symbol)
type error
[4 r] : (list (not string))
[4 r] : (list (not string))
|
|