		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 (emptyp 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-emptyp

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