		Search-engine friendly clone of the ACL2 documentation.

Fty::basetypes

A book that associates many built-in ACL2 predicates with suitable fixing functions and equivalence relations, for use in the fty-discipline.

The centaur/fty/basetypes book provides basic support for using many built-in ACL2 types with the FTY discipline. It introduces any necessary fixing functions and equivalences, and then sets up fty::deffixtype associations between the recognizers, fixing functions, and equivalence relations for the following types.

See also fty::baselists, which sets up similar support for various built-in list recognizers like character-listp, etc.

Type Name	Recognizer	Fix	Equiv
bit	bitp	bfix	`bit-equiv`
nat	natp	nfix	`nat-equiv`
int	integerp	ifix	`int-equiv`
rational	rationalp	rfix	`rational-equiv`
acl2-number	ACL2-numberp	fix	`number-equiv`
true-list	true-listp	list-fix	`list-equiv`
string	stringp	str-fix	`streqv`
true	true-p	true-fix	`true-equiv`
symbol	symbolp	symbol-fix	`symbol-equiv`
pos	posp	pos-fix	`pos-equiv`
character	characterp	char-fix	`chareqv`
any	any-p	identity	`equal`
bool	booleanp	bool-fix	`iff`
maybe-nat	maybe-natp	maybe-natp-fix	`maybe-nat-equiv`
maybe-pos	maybe-posp	maybe-posp-fix	`maybe-pos-equiv`
maybe-bit	maybe-bitp	maybe-bit-fix	`maybe-bit-equiv`
maybe-integer	maybe-integerp	maybe-integerp-fix	`maybe-integer-equiv`

Note: all of these associations are made in the ACL2 package.

Subtopics

Any-p: (any-p x) is always true; i.e., it recognizes any ACL2 object.
Symbol-fix: (symbol-fix x) is a fixing function for symbolp; it is the identity for symbols and coerces non-symbols to acl2::||, i.e., the empty symbol in the ACL2 package.
Maybe-integerp-fix: (maybe-integerp-fix x) is the identity for maybe-integerps, or coerces any invalid object to nil.
Maybe-integer-equiv: (maybe-integerp-equiv x y) is an equivalence relation for maybe-integerps, i.e., equality up to maybe-integerp-fix.
Maybe-posp-fix: (maybe-posp-fix x) is the identity for maybe-posps, or coerces any non-posp to nil.
Maybe-natp-fix: (maybe-natp-fix x) is the identity for maybe-natps, or coerces any invalid object to nil.
Maybe-bit-fix: (maybe-bit-fix x) is the identity for maybe-bitps, or coerces any non-bitp to nil.
Bool-fix: (bool-fix x) is a fixing function for Booleans; it coerces any non-nil symbol to t.
Maybe-pos-equiv: (maybe-posp-equiv x y) is an equivalence relation for maybe-posps, i.e., equality up to maybe-posp-fix.
Maybe-nat-equiv: (maybe-natp-equiv x y) is an equivalence relation for maybe-natps, i.e., equality up to maybe-natp-fix.
Maybe-bit-equiv: (maybe-bitp-equiv x y) is an equivalence relation for maybe-bitps, i.e., equality up to maybe-bit-fix.
Maybe-lit-fix: (maybe-lit-fix x) is the identity for maybe-litps, or coerces any non-litp to nil.
Symbol-equiv: (symbol-equiv x y) recognizes symbols that are identical under symbol-fix.
True-equiv: (true-equiv x y) is a ``degenerate'' equivalence for true-p objects.
Pos-equiv: (pos-equiv x y) is equality for positive numbers, i.e., equality up to pos-fix.
Lposfix: (lposfix x) is logically identical to (pos-fix x), but its guard requires that x is a posp and, in the execution, it's just a no-op that returns x.
True-p: (true-p x) recognizes only the symbol t.
True-fix: (true-fix x) ignores its argument and unconditionally returns t.