		Search-engine friendly clone of the ACL2 documentation.

Primitives

Sfix

(sfix x) is a fixing function for sets.

We return any proper setp unchanged, but coerce any non-setp into the empty set.

This does for sets what functions like nfix or rfix do for numbers. It is often useful to use sfix in the base case of a set operation to ensure that an ordered set is always produced.

Definitions and Theorems

Function: sfix

(defun sfix (x)
       (declare (xargs :guard (setp x)))
       (mbe :logic (if (empty x) nil x)
            :exec x))

Theorem: sfix-produces-set

(defthm sfix-produces-set (setp (sfix x)))

Theorem: sfix-set-identity

(defthm sfix-set-identity
        (implies (setp x) (equal (sfix x) x)))

Theorem: sfix-when-empty

(defthm sfix-when-empty
        (implies (empty x)
                 (equal (sfix x) nil)))