		Search-engine friendly clone of the ACL2 documentation.

Deffixequiv-sk

A variant of deffixequiv for defun-sk functions.

Introduction

The macro deffixequiv automates the generation of theorems saying that a function fixes its arguments to certain types. That macro provides the ability to supply hints, which are often not needed if the function explicitly fixes the arguments (by calling fixing functions) or implicitly does so by calling functions that do (for which the fixing theorems have already been proved.

However, when defun-sk functions similarly, explicitly or implicitly, fix their arguments, hints are needed in order to prove the fixing theorems. Unsurprisingly, these hints have a boilerplate form that can be derived from the function.

This macro, deffixequiv-sk, generates these hints. More precisely, it generates a deffixequiv that includes the hints derived from the function.

If you find that this macro fails, please notify the implementor. Future versions of this macro may also allow the user to specify additional hints (besides the generated ones) to help prove the fixing properties.

General Form

(deffixequiv-sk fn
                :args ((arg1 pred1) ... (argn predn))  ; default nil
  )

Inputs

A symbol that specifies the defun-sk function.

:args — default nil

A list of doublets ((arg1 pred1) ... (argn predn)) where each argi is an argument of fn and predi is the predicate that the argument is fixed to. The argi symbols must all be distinct.
This syntax is similar to deffixequiv. Note that the predi symbols must be predicates, not fixtype names.

Generated Events

A call

(deffixequiv :args ((arg1 pred1) ... (argn predn)) :hints ...)

where ... are hints generated from the function. The exact form of and motivation for these hints will be described in upcoming extensions of this documentation.

Subtopics

Deffixequiv-sk-implementation: Implementation of deffixequiv-sk.