• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • 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
        • One-way-unify$
        • Check-unary-lambda-call
        • 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
        • If-tree-leaf-terms
        • Check-not-call
        • Check-mbt-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
      • Install-not-normalized-event-lst
      • Std/system/term-function-recognizers
      • Genvar$
      • Std/system/event-name-queries
      • Pseudo-tests-and-call-listp
      • Maybe-pseudo-event-formp
      • Add-suffix-to-fn-or-const
      • Chk-irrelevant-formals-ok
      • Table-alist+
      • Pseudo-tests-and-callp
      • 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-command-landmark-listp
      • Install-not-normalized$
      • Pseudo-event-landmark-listp
      • Known-packages
      • Std/system/partition-rest-and-keyword-args
      • Rune-enabledp
      • Rune-disabledp
      • Included-books
      • Std/system/pseudo-event-formp
      • Std/system/plist-worldp-with-formals
      • Std/system/w
      • Std/system/geprops
      • Std/system/arglistp
      • Std/system/constant-queries
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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.

One-way-unify$

A logic-mode guard-verified version of one-way-unify.

Check-unary-lambda-call

Check if a term is a (translated) call of a unary lambda expression.

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$.

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.

Check-mbt-call

Check if a term is a call of mbt.

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.