# 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

fn

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`.