Top

Smtlink-hint

Decl

This is a product type introduced by defprod.

Fields

name — symbolp
type — hint-pair

Additional Requirements

The following invariant is enforced on the fields:

(symbolp (hint-pair->thm type))

Subtopics

Decl-fix: Fixing function for decl structures.
Decl-equiv: Basic equivalence relation for decl structures.
Make-decl: Basic constructor macro for decl structures.
Decl->type: Get the type field from a decl.
Change-decl: Modifying constructor for decl structures.
Decl->name: Get the name field from a decl.
Decl-p: Recognizer for decl structures.
Decl-list: A list of decl-p objects.