Sfix
Fixer for sets.
- Signature
(sfix set) → set$
- Arguments
- set — Guard (setp set).
- Returns
- set$ — Type (setp set$).
Definitions and Theorems
Function: sfix
(defun sfix (set)
(declare (xargs :guard (setp set)))
(mbe :logic (if (setp set) set nil)
:exec (the (or cons null) set)))
Theorem: setp-of-sfix
(defthm setp-of-sfix
(b* ((set$ (sfix set))) (setp set$))
:rule-classes :rewrite)
