		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Get-leftmost-nonconst

Return the leftmost term in a list that is not a quoted constant.

Signature
(get-leftmost-nonconst terms) → term?
Arguments: terms — Guard (tterm-listp terms).
Returns: term? — Type (tterm-optionp term?).

This is used as explained in step-from-trans.

If there is no such term, we return nil. Note that nil is not a term in our formalization of terms.

Definitions and Theorems

Function: get-leftmost-nonconst

(defun get-leftmost-nonconst (terms)
       (declare (xargs :guard (tterm-listp terms)))
       (let ((__function__ 'get-leftmost-nonconst))
            (declare (ignorable __function__))
            (b* (((when (endp terms)) nil)
                 (term (car terms))
                 ((when (tterm-case term :constant))
                  (get-leftmost-nonconst (cdr terms))))
                (tterm-fix term))))

Theorem: tterm-optionp-of-get-leftmost-nonconst

(defthm tterm-optionp-of-get-leftmost-nonconst
        (b* ((term? (get-leftmost-nonconst terms)))
            (tterm-optionp term?))
        :rule-classes :rewrite)

Theorem: tterm-case-constant-listp-when-not-get-leftmost-nonconst

(defthm tterm-case-constant-listp-when-not-get-leftmost-nonconst
        (implies (and (tterm-listp terms)
                      (not (ttermp (get-leftmost-nonconst terms))))
                 (tterm-case-constant-listp terms)))

Theorem: get-leftmost-nonconst-of-tterm-list-fix-terms

(defthm get-leftmost-nonconst-of-tterm-list-fix-terms
        (equal (get-leftmost-nonconst (tterm-list-fix terms))
               (get-leftmost-nonconst terms)))

Theorem: get-leftmost-nonconst-tterm-list-equiv-congruence-on-terms

(defthm get-leftmost-nonconst-tterm-list-equiv-congruence-on-terms
        (implies (tterm-list-equiv terms terms-equiv)
                 (equal (get-leftmost-nonconst terms)
                        (get-leftmost-nonconst terms-equiv)))
        :rule-classes :congruence)