		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Finalization

Fixtype of finalizations.

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

Fields

command — finalize-command
finalizer — finalizer

This notion is not explicitly named in the grammar, but it is the optional thing that may conclude a function. It consists of a finalization command and a finalizer.

Subtopics

Finalization-fix: Fixing function for finalization structures.
Finalization-equiv: Basic equivalence relation for finalization structures.
Make-finalization: Basic constructor macro for finalization structures.
Finalization->finalizer: Get the finalizer field from a finalization.
Finalization->command: Get the command field from a finalization.
Change-finalization: Modifying constructor for finalization structures.
Finalizationp: Recognizer for finalization structures.