Top

Smtlink-hint

Func

This is a product type introduced by defprod.

Fields

name — symbolp
formals — decl-list
guard — hint-pair
returns — decl-list
more-returns — hint-pair-list
expansion-depth — natp
flattened-formals — ACL2::symbol-list
flattened-returns — ACL2::symbol-list

Subtopics

Func-fix: Fixing function for func structures.
Func-p: Recognizer for func structures.
Make-func: Basic constructor macro for func structures.
Func-equiv: Basic equivalence relation for func structures.
Func->flattened-returns: Get the flattened-returns field from a func.
Func->flattened-formals: Get the flattened-formals field from a func.
Change-func: Modifying constructor for func structures.
Func->more-returns: Get the more-returns field from a func.
Func->expansion-depth: Get the expansion-depth field from a func.
Func->returns: Get the returns field from a func.
Func->formals: Get the formals field from a func.
Func->name: Get the name field from a func.
Func->guard: Get the guard field from a func.
Func-list: A list of func-p objects.