Fixtype of frames.
This is a product type introduced by fty::defprod.
- 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.
- Fixing function for frame structures.
- Basic equivalence relation for frame structures.
- Basic constructor macro for frame structures.
- Get the binding field from a frame.
- Modifying constructor for frame structures.
- Get the term field from a frame.
- Recognizer for frame structures.