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

The

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

Type Name | Recognizer | Fix | Equiv |
---|---|---|---|

bitp | bfix | bit-equiv | |

natp | nfix | nat-equiv | |

integerp | ifix | int-equiv | |

rationalp | rfix | rational-equiv | |

ACL2-numberp | fix | number-equiv | |

true-listp | list-fix | list-equiv | |

stringp | str-fix | streqv | |

true-p | true-fix | true-equiv | |

symbolp | symbol-fix | symbol-equiv | |

posp | pos-fix | pos-equiv | |

characterp | char-fix | chareqv | |

any-p | identity | equal | |

booleanp | bool-fix | iff | |

maybe-natp | maybe-natp-fix | maybe-nat-equiv | |

maybe-posp | maybe-posp-fix | maybe-pos-equiv | |

maybe-bitp | maybe-bit-fix | maybe-bit-equiv | |

maybe-integerp | maybe-integerp-fix | maybe-integer-equiv |

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

- 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 toacl2::|| , 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 tonil .- 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 tonil .- Maybe-natp-fix
`(maybe-natp-fix x)`is the identity for maybe-natps, or coerces any invalid object tonil .- Maybe-bit-fix
`(maybe-bit-fix x)`is the identity for maybe-bitps, or coerces any non-bitp tonil .- Bool-fix
`(bool-fix x)`is a fixing function for Booleans; it coerces any non-nil symbol tot .- 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 tonil .- 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 thatx is a posp and, in the execution, it's just a no-op that returnsx .- True-p
`(true-p x)`recognizes only the symbolt .- True-fix
`(true-fix x)`ignores its argument and unconditionally returnst .