		Search-engine friendly clone of the ACL2 documentation.

Std/util

Deffixer

Introduce a fixer for a predicate.

Introduction

Given a unary predicate, a fixer (i.e. fixing function) for the predicate can be defined in a standard way. This macro automates this.

This macro may be extended to accommodate variations in the definition of fixers.

General Form

(deffixer name
          :pred ...
          :param ...
          :body-fix ...
          :parents ...
          :short ...
          :long ...
  )

Inputs

name

A symbol that specifies the name of the fixer.

:pred

A symbol that names a unary predicate. This is the predicate that the fixer is for.

:param

The formal parameter to use for the fixer.
If not supplied, it defaults to x, in the same package as name.

:body-fix

A term that defines the value of the fixer when the argument is not in the predicate. Its only free variables, if any, must be just the parameter of the fixer (see :param). It must be the case that this term satisfies the predicate when the parameter of the fixer does not.

:parents
:short
:long

These, if present, are added to the XDOC topic generated for the fixer.

Generated Events

name

The fixer, with the predicate as guard and the following body:
(mbe :logic (if (pred param) param body-fix)
     :exec param)

pred-of-name

A rewrite rule asserting that the fixer always satisfies the predicate:
(pred (name param))

pred-when-name

A rewrite rule asserting that the fixer rewrites to the parameter when the predicate holds:
(implies (pred param)
         (equal (name param)
                param))

The above items are generated in a define for the fixer.

Subtopics

Deffixer-implementation: Implementation of deffixer.
Defconstrained-recognizer-implementation: Implementation of defconstrained-recognizer.