A variant of deffixequiv for defun-sk functions.
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.
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.
(deffixequiv-sk fn :args ((arg1 pred1) ... (argn predn)) ; default nil )
A symbol that specifies the defun-sk function.
A list of doublets
((arg1 pred1) ... (argn predn))where each argiis an argument of fnand prediis the predicate that the argument is fixed to. The argisymbols must all be distinct.
This syntax is similar to deffixequiv. Note that the
predisymbols must be predicates, not fixtype names.
(deffixequiv :args ((arg1 pred1) ... (argn predn)) :hints ...)