		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Operations on the Syntheto abstract syntax.

These are operations to query and manipulate the syntax. We will add more as needed.

Subtopics

Subst-expression-fns: Mutually recursive functions for expression substitution.
Field-list-to-typed-variable-list: Lift field-to-typed-variable to lists.
Negate-expression: Negate an expression.
Get-function-definition-in-function-definitions: Find the definition of a function with a given name in a list of function definitions.
Get-function-definition: Find the definition of a function with a given name in a list of top-level constructs.
Get-type-definition-in-type-definitions: Find the definition of a type with a given name in a list of type definitions.
Get-type-definition: Find the definition of a type with a given name in a list of top-level constructs.
Get-function-specification: Find the function specification with a given name in a list of top-level constructs.
Get-type-subset: Return the type subset that defines a type, if any.
Get-alternative-product: Find the type product of the alternative with a specified name.
Direct-supertype: Return the direct supertype of a type, if any.
Get-function-header-in-list: Find the function header with a given name in a list of function headers.
Equate-expression-lists: Construct a list of equalities between two lists of expressions, element-wise.
Get-field-type: Find the type of the field with a specified name.
Get-theorem: Find the theorem with a given name in a list of top-level constructs.
Get-defined-type-names-in-type-definitions: Return the list of the type names defined in a list of definitions, in the same order.
Disjoin-expressions: Disjoin a list of expressions.
Conjoin-expressions: Conjoin a list of expressions.
Get-type-product: Return the type product that defines a type, if any.
Binary-op-nonstrictp: Check if a binary operator is non-strict.
Get-type-sum: Return the type sum that defines a type, if any.
Get-defined-type-names: Return the list of the type names defined in a list of top-level constructs, in the same order.
Equate-expressions: Construct an equality between two expressions.
Field-to-typed-variable: Turn a field into a typed variable.
Subst-expression: Apply a substitution to an expression.
Binary-op-strictp: Check if a binary operator is strict.
Initializer-list-from-flds-vals
Typed-variable-list->-expression-variable-list
Typed-variable-list->-expression
Variable-substitution: Fixtype of variable substitutions.
Local-variables
Identifier-list-names
Functions-called
Subst-expression-list: Apply a substitution to a list of expressions.
Subst-branch-list: Apply a substitution to a list of branches.
Subst-branch: Apply a substitution to a branch.