Utilities to query terms.

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