Get the constraints field from a vttree-constraints.
(vttree-constraints->constraints x) → constraints
This is an ordinary field accessor created by defprod.
Function:
(defun vttree-constraints->constraints$inline (x) (declare (xargs :guard (vttree-p x))) (declare (xargs :guard (equal (vttree-kind x) :constraints))) (let ((__function__ 'vttree-constraints->constraints)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and (equal (vttree-kind x) :constraints) x))) (sv::constraintlist-fix (cdr x))) :exec (cdr x))))
Theorem:
(defthm constraintlist-p-of-vttree-constraints->constraints (b* ((constraints (vttree-constraints->constraints$inline x))) (sv::constraintlist-p constraints)) :rule-classes :rewrite)
Theorem:
(defthm vttree-constraints->constraints$inline-of-vttree-fix-x (equal (vttree-constraints->constraints$inline (vttree-fix x)) (vttree-constraints->constraints$inline x)))
Theorem:
(defthm vttree-constraints->constraints$inline-vttree-equiv-congruence-on-x (implies (vttree-equiv x x-equiv) (equal (vttree-constraints->constraints$inline x) (vttree-constraints->constraints$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm vttree-constraints->constraints-when-wrong-kind (implies (not (equal (vttree-kind x) :constraints)) (equal (vttree-constraints->constraints x) (sv::constraintlist-fix nil))))