		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Function

Fixtype of functions.

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

Fields

name — identifier
inputs — function-input-list
instrs — instruction-list
outputs — function-output-list
finalize — finalization

A function consists of a name (identifier), inputs, instructions, outputs, and an optional finalization. Here we do not capture the requirement that there is at least an instruction.

Subtopics

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