• 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
        • Std/system/term-transformations
          • Make-mv-let-call
          • Mvify
          • 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
          • Apply-fn-into-ifs
          • Conjoin-equalities
          • Fapply-unary-to-terms
          • Apply-unary-to-terms
          • Apply-terms-same-args
          • Apply-term
          • Fsublis-fn-lst-simple
          • Fsublis-fn
          • Fapply-terms-same-args
          • Fsublis-fn-simple
          • Fapply-term
          • Remove-mbe-logic
          • Remove-mbe-exec
          • Quote-term
          • Quote-term-list
          • Apply-term*
          • Std/system/fsubcor-var
          • Std/system/conjoin
          • Std/system/flatten-ands-in-lit
          • Fapply-term*
          • Std/system/dumb-negate-lit
        • 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-transformations

Utilities to transform terms.

Subtopics

Make-mv-let-call
Build a translated call of mv-let.
Mvify
Turn a single-value term into a multi-value term.
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)).
Apply-fn-into-ifs
Apply a function symbol or lambda expression to the term, pushing the function into the if branches.
Conjoin-equalities
Build a conjunction of equalities with the given left-hand and right-hand sides.
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.
Fsublis-fn-simple
Variant of sublis-fn-simple that performs no simplification.
Fapply-term
Variant of apply-term 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
Build a quoted constant term with the given value.
Quote-term-list
Lift quote-term to lists.
Apply-term*
Apply a function symbol or a lambda expression to zero or more terms, obtaining a term.
Std/system/fsubcor-var
Theorems about fsubcor-var.
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.