Frame
Fixtype of frames.
This is a product type introduced by fty::defprod.
Fields
- term — tterm
- binding — binding
The evaluation of ACL2 terms is naturally described via a stack.
Here we formalize the frames (i.e. elements) of this stack.
A frame consists of a term under evaluation
and a binding for (normally) at least the variables in the term.
Subtopics
- Frame-fix
- Fixing function for frame structures.
- Frame-equiv
- Basic equivalence relation for frame structures.
- Make-frame
- Basic constructor macro for frame structures.
- Frame->binding
- Get the binding field from a frame.
- Change-frame
- Modifying constructor for frame structures.
- Frame->term
- Get the term field from a frame.
- Framep
- Recognizer for frame structures.
