Top

Smtlink-hint

Let-binding

This is a product type introduced by defprod.

Fields

bindings — binding-list
hypotheses — hint-pair-list

Subtopics

Let-binding-fix: Fixing function for let-binding structures.
Let-binding-equiv: Basic equivalence relation for let-binding structures.
Make-let-binding: Basic constructor macro for let-binding structures.
Let-binding->hypotheses: Get the hypotheses field from a let-binding.
Let-binding->bindings: Get the bindings field from a let-binding.
Change-let-binding: Modifying constructor for let-binding structures.
Let-binding-p: Recognizer for let-binding structures.