		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)