		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-add-qconstants-in-term

Collect all the quoted constants in a term.

Signature
(atj-add-qconstants-in-term term qconsts) → new-qconsts
Arguments: term — Guard (pseudo-termp term).; qconsts — Guard (atj-qconstants-p qconsts).
Returns: new-qconsts — Type (atj-qconstants-p new-qconsts), given (atj-qconstants-p qconsts).

We return all the values of the quoted constants that appear directly quoted in the term. That is, for each sub-term of the form (quote <value>), we return <value>. This excludes value that occur (only) inside other quoted values, e.g. (quote (<value> . ...)).

The record that stores the collected constants is threaded through the recursive functions.

Theorem: return-type-of-atj-add-qconstants-in-term.new-qconsts

(defthm return-type-of-atj-add-qconstants-in-term.new-qconsts
 (implies
      (atj-qconstants-p qconsts)
      (b* ((?new-qconsts (atj-add-qconstants-in-term term qconsts)))
        (atj-qconstants-p new-qconsts)))
 :rule-classes :rewrite)

Theorem: return-type-of-atj-add-qconstants-in-terms.new-qconsts

(defthm return-type-of-atj-add-qconstants-in-terms.new-qconsts
 (implies
    (atj-qconstants-p qconsts)
    (b* ((?new-qconsts (atj-add-qconstants-in-terms terms qconsts)))
      (atj-qconstants-p new-qconsts)))
 :rule-classes :rewrite)

Subtopics

Atj-add-qconstants-in-terms