• 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
      • Std/system/term-transformations
        • Mvify
        • Make-mv-let-call
        • Remove-trivial-vars
        • Remove-unused-vars
        • Fsublis-fn-rec
        • Close-lambdas
        • Fsublis-var
        • Remove-mbe-logic/exec
        • Untranslate$
        • Remove-dead-if-branches
        • Remove-progn
        • Make-mv-nth-calls
        • Conjoin-equalities
        • Apply-fn-into-ifs
        • Fapply-unary-to-terms
        • Apply-unary-to-terms
        • Apply-terms-same-args
        • Apply-term
        • Fsublis-fn-lst-simple
        • Fsublis-fn
        • Fapply-terms-same-args
        • Fapply-term
        • Fsublis-fn-simple
        • Remove-mbe-logic
        • Remove-mbe-exec
        • Quote-term-list
        • Quote-term
        • Apply-term*
        • Std/system/conjoin
        • Std/system/flatten-ands-in-lit
        • Fapply-term*
        • Std/system/dumb-negate-lit
      • 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-transformations

Utilities to transform terms.

Subtopics

Mvify

Turn a single-value term into a multi-value term.

Make-mv-let-call

Build a translated call of mv-let.

Remove-trivial-vars

Remove the trivial lambda-bound variables.

Remove-unused-vars

Remove all the lambda-bound variables that are not used.

Fsublis-fn-rec

Variant of sublis-fn-rec that performs no simplification.

Close-lambdas

Make all the lambda expressions in a term closed.

Fsublis-var

Variant of sublis-var that performs no simplification.

Remove-mbe-logic/exec

Turn every call (mbe :logic a :exec b) in a term into just its :logic part a or :exec part b.

Untranslate$

A logic-mode guard-verified version of untranslate.

Remove-dead-if-branches

Remove all the dead if bramches in a term.

Remove-progn

Turn every call of prog2$ and progn$ in a term into just its last argument.

Make-mv-nth-calls

Given a term term, return the list of n terms ((mv-th '0 term) ... (mv-nth 'n-1 term)).

Conjoin-equalities

Build a conjunction of equalities with the given left-hand and right-hand sides.

Apply-fn-into-ifs

Apply a function symbol or lambda expression to the term, pushing the function into the if branches.

Fapply-unary-to-terms

Variant of apply-unary-to-terms that performs no simplification.

Apply-unary-to-terms

Apply a function symbol or a unary lambda expression to each element of a list of terms, obtaining a list of corresponding terms.

Apply-terms-same-args

Apply each function symbol or lambda expression of a list to the same list of pseudo-term arguments, obtaining a list of corresponding function applications.

Apply-term

Apply a function symbol or a lambda expression to a list of terms, obtaining a term.

Fsublis-fn-lst-simple

Variant of sublis-fn-lst-simple that performs no simplification.

Fsublis-fn

Variant of sublis-fn that performs no simplification.

Fapply-terms-same-args

Variant of apply-terms-same-args that performs no simplification.

Fapply-term

Variant of apply-term that performs no simplification.

Fsublis-fn-simple

Variant of sublis-fn-simple that performs no simplification.

Remove-mbe-logic

Turn every call (mbe :logic a :exec b) in a term into just its :exec part b.

Remove-mbe-exec

Turn every call (mbe :logic a :exec b) in a term into just its :logic part a.

Quote-term-list

Lift quote-term to lists.

Quote-term

Build a quoted constant term with the given value.

Apply-term*

Apply a function symbol or a lambda expression to zero or more terms, obtaining a term.

Std/system/conjoin

Theorems about conjoin and conjoin2.

Std/system/flatten-ands-in-lit

Theorems about flatten-ands-in-lit.

Fapply-term*

Variant of apply-term* that performs no simplification.

Std/system/dumb-negate-lit

Theorems about dumb-negate-lit.