Environment extension for ext
theorems #
Information about an extensionality theorem, stored in the environment extension.
- declName : Name
Declaration name of the extensionality theorem.
- priority : Nat
Priority of the extensionality theorem.
- keys : Array DiscrTree.Key
Key in the discrimination tree, for the type in which the extensionality theorem holds.
Instances For
The state of the ext
extension environment
- tree : DiscrTree ExtTheorem
The tree of
ext
extensions. Erased
ext
s viaattribute [-ext]
.
Instances For
The environment extension to track @[ext]
theorems.
Gets the list of @[ext]
theorems corresponding to the key ty
,
ordered from high priority to low.
Equations
Instances For
Erases a name marked ext
by adding it to the state's erased
field and
removing it from the state's list of Entry
s.
This is triggered by attribute [-ext] name
.
Equations
Instances For
Erases a name marked as a ext
attribute.
Check that it does in fact have the ext
attribute by making sure it names a ExtTheorem
found somewhere in the state's tree, and is not erased.