		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Constraint-constrels

Set of relation constraints in a constraint.

Signature
(constraint-constrels constr) → crels
Arguments: constr — Guard (constraintp constr).
Returns: crels — Type (constrel-setp crels).

This is the empty set for an equality constraints; for a relation constraint, it is the singleton with that constraint, in constrel form. This function is used to define constraint-list-constrels.

Definitions and Theorems

Function: constraint-constrels

(defun constraint-constrels (constr)
  (declare (xargs :guard (constraintp constr)))
  (let ((__function__ 'constraint-constrels))
    (declare (ignorable __function__))
    (constraint-case
         constr
         :equal nil
         :relation (insert (make-constrel :name constr.name
                                          :args constr.args)
                           nil))))

Theorem: constrel-setp-of-constraint-constrels

(defthm constrel-setp-of-constraint-constrels
  (b* ((crels (constraint-constrels constr)))
    (constrel-setp crels))
  :rule-classes :rewrite)

Theorem: constraint-constrels-of-constraint-fix-constr

(defthm constraint-constrels-of-constraint-fix-constr
  (equal (constraint-constrels (constraint-fix constr))
         (constraint-constrels constr)))

Theorem: constraint-constrels-constraint-equiv-congruence-on-constr

(defthm constraint-constrels-constraint-equiv-congruence-on-constr
  (implies (constraint-equiv constr constr-equiv)
           (equal (constraint-constrels constr)
                  (constraint-constrels constr-equiv)))
  :rule-classes :congruence)