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.
(1+) (datatype not
X : A; !; fail!;
_____________________
X : (mode (not A) -);
_____________________
X : (mode (not A) -);)
type#my-prover-types : symbol
(2+) f : (not number)
f : (not number)
(3+) f : (not symbol)
type error
(4+) [4 r] : (list (not string))
[4 r] : (list (not string))
|
|
