Accessor for the value of a null or quote pseudo-term.
(pseudo-term-const->val x) → *
Function:
(defun pseudo-term-const->val (x) (declare (xargs :guard (pseudo-termp x))) (declare (xargs :guard (member-eq (pseudo-term-kind x) '(:quote :null)))) (let ((__function__ 'pseudo-term-const->val)) (declare (ignorable __function__)) (mbe :logic (and (eq (pseudo-term-kind x) :quote) (pseudo-term-quote->val x)) :exec (cadr x))))
Theorem:
(defthm pseudo-term-const->val-when-quote (implies (equal (pseudo-term-kind x) :quote) (equal (pseudo-term-const->val x) (pseudo-term-quote->val x))))
Theorem:
(defthm pseudo-term-const->val-when-not-quote (implies (not (equal (pseudo-term-kind x) :quote)) (equal (pseudo-term-const->val x) nil)))
Theorem:
(defthm pseudo-term-const->val-of-pseudo-term-fix-x (equal (pseudo-term-const->val (pseudo-term-fix x)) (pseudo-term-const->val x)))
Theorem:
(defthm pseudo-term-const->val-pseudo-term-equiv-congruence-on-x (implies (pseudo-term-equiv x x-equiv) (equal (pseudo-term-const->val x) (pseudo-term-const->val x-equiv))) :rule-classes :congruence)