|
|
|---|
|
|
|
|---|
Fixtype of values and errors.
This is a sum-of-products (i.e., union) type, introduced by fty::defflexsum.
Theorem:
(defthm not-errorp-when-valuep (implies (valuep x) (not (errorp x))))
Theorem:
(defthm errorp-when-value-resultp-and-not-valuep (implies (and (value-resultp x) (not (valuep x))) (errorp x)))