		Search-engine friendly clone of the ACL2 documentation.

Functions

Function

Fixtype of (defined) functions.

This is a product type introduced by fty::defprod.

Fields

name — symbol-value
params — symbol-value-list
body — tterm

We use our model of symbol values, and not ACL2 symbols directly, because we want to represent all possible functions, not just the ones whose name and parameters are symbols in known packages. This is similar to the use of symbol values in translated terms; see tterm.

Subtopics

Function-fix: Fixing function for function structures.
Function-equiv: Basic equivalence relation for function structures.
Make-function: Basic constructor macro for function structures.
Function->params: Get the params field from a function.
Change-function: Modifying constructor for function structures.
Function->name: Get the name field from a function.
Function->body: Get the body field from a function.
Functionp: Recognizer for function structures.