• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/io
      • Std/osets
      • Std/system
        • Fresh-logical-name-with-$s-suffix
        • Irrelevant-formals-info
        • Std/system/function-queries
        • Std/system/term-queries
          • Check-mv-let-call
          • Term-possible-numbers-of-results
          • Check-user-term
          • Check-nary-lambda-call
          • Check-lambda-call
          • All-vars-open
          • Dumb-occur-var-open
          • Check-user-lambda
          • Check-if-call
          • Check-unary-lambda-call
          • One-way-unify$
          • Guard-verified-fnsp
          • All-non-gv-ffn-symbs
          • All-non-gv-exec-ffn-symbs
          • Check-fn-call
          • Guard-verified-exec-fnsp
          • Check-list-call
          • Check-or-call
          • Check-and-call
          • All-program-ffn-symbs
          • Lambda-guard-verified-fnsp
          • All-free/bound-vars
          • Check-mbt$-call
          • Check-mbt-call
          • If-tree-leaf-terms
          • Check-not-call
          • Term-guard-obligation
          • All-pkg-names
          • All-vars-in-untranslated-term
          • Std/system/all-fnnames
          • Lambda-logic-fnsp
          • Lambda-guard-verified-exec-fnsp
          • All-lambdas
          • Lambda-closedp
          • Std/system/all-vars
        • Std/system/term-transformations
        • Std/system/enhanced-utilities
        • Install-not-normalized-event-lst
        • Install-not-normalized-event
        • Std/system/term-function-recognizers
        • Pseudo-tests-and-call-listp
        • Genvar$
        • Std/system/event-name-queries
        • Maybe-pseudo-event-formp
        • Add-suffix-to-fn-or-const
        • Chk-irrelevant-formals-ok
        • Std/system/good-atom-listp
        • Pseudo-tests-and-callp
        • Table-alist+
        • Add-suffix-to-fn-or-const-lst
        • Known-packages+
        • Add-suffix-to-fn-lst
        • Unquote-term
        • Event-landmark-names
        • Add-suffix-lst
        • Std/system/theorem-queries
        • Unquote-term-list
        • Std/system/macro-queries
        • Pseudo-event-landmark-listp
        • Pseudo-command-landmark-listp
        • Install-not-normalized$
        • Rune-disabledp
        • Known-packages
        • Std/system/partition-rest-and-keyword-args
        • Rune-enabledp
        • Included-books
        • Std/system/pseudo-event-formp
        • Std/system/plist-worldp-with-formals
        • Std/system/w
        • Std/system/geprops
        • Std/system/arglistp
        • Std/system-extensions
        • Std/system/constant-queries
      • Std/basic
      • Std/typed-lists
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
      • Std-extensions
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Std/system

Std/system/term-queries

Utilities to query terms.

Subtopics

Check-mv-let-call
Check if a term is a (translated) call of mv-let.
Term-possible-numbers-of-results
Calculate the possible numbers of results of a translated term.
Check-user-term
Recognize untranslated terms that are valid for evaluation.
Check-nary-lambda-call
Check if a term is a (translated) call of an n-ary lambda expression.
Check-lambda-call
Check if a term is a (translated) call of a lambda expression.
All-vars-open
Free variables in a term that may contain non-closed (i.e. open) lambda expressions.
Dumb-occur-var-open
Check if a variable occurs free in a term that may contain non-closed (i.e. open) lambda expressions.
Check-user-lambda
Recognize untranslated lambda expressions that are valid for evaluation.
Check-if-call
Check if a term is a call of if.
Check-unary-lambda-call
Check if a term is a (translated) call of a unary lambda expression.
One-way-unify$
A logic-mode guard-verified version of one-way-unify.
Guard-verified-fnsp
Check if a term calls only guard-verified functions.
All-non-gv-ffn-symbs
Non-guard-verified functions called by a term.
All-non-gv-exec-ffn-symbs
Non-guard-verified functions called by a term for execution.
Check-fn-call
Check if a term is a (translated) call of a named function.
Guard-verified-exec-fnsp
Check if a term calls only guard-verified functions for execution.
Check-list-call
Check if a term is a (translated) call of list.
Check-or-call
Check if a term is a (translated) call of or.
Check-and-call
Check if a term is a (translated) call of and.
All-program-ffn-symbs
Program-mode functions called by a term.
Lambda-guard-verified-fnsp
Check if all the functions in a lambda expression are guard-verified.
All-free/bound-vars
Return all the free and bound variables that occur in a term.
Check-mbt$-call
Check if a term is a call of mbt$.
Check-mbt-call
Check if a term is a call of mbt.
If-tree-leaf-terms
Collect the leaf terms according to the if tree structure of a term.
Check-not-call
Check if a term is a call of not.
Term-guard-obligation
Formula expressing the guard obligation of a term.
All-pkg-names
Collect all the package names of all the symbols in a term.
All-vars-in-untranslated-term
The variables free in the given untranslated term.
Std/system/all-fnnames
Theorems about all-fnnames.
Lambda-logic-fnsp
Check if a lambda expression is in logic mode, i.e. its body is in logic mode.
Lambda-guard-verified-exec-fnsp
Check if a lambda expression calls only guard-verified functions for execution.
All-lambdas
Lambda expressions in a term.
Lambda-closedp
Check if a lambda expression is closed, i.e. it has no free variables.
Std/system/all-vars
Theorems about all-vars.