Environment extension for ext theorems

structure Lean.Meta.Ext.ExtTheorem : Type

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.

instance Lean.Meta.Ext.instInhabitedExtTheorem : Inhabited ExtTheorem

instance Lean.Meta.Ext.instReprExtTheorem : Repr ExtTheorem

instance Lean.Meta.Ext.instBEqExtTheorem : BEq ExtTheorem

instance Lean.Meta.Ext.instHashableExtTheorem : Hashable ExtTheorem

structure Lean.Meta.Ext.ExtTheorems : Type

The state of the ext extension environment

• tree : DiscrTree ExtTheorem

  The tree of ext extensions.

• erased : PHashSet Name

  Erased exts via attribute [-ext].

instance Lean.Meta.Ext.instInhabitedExtTheorems : Inhabited ExtTheorems

opaque Lean.Meta.Ext.extExtension : SimpleScopedEnvExtension ExtTheorem ExtTheorems

The environment extension to track @[ext] theorems.

@[inline]

def Lean.Meta.Ext.getExtTheorems (ty : Expr) : MetaM (Array ExtTheorem)

Gets the list of @[ext] theorems corresponding to the key ty, ordered from high priority to low.

def Lean.Meta.Ext.ExtTheorems.eraseCore (d : ExtTheorems) (declName : Name) : ExtTheorems

Erases a name marked ext by adding it to the state's erased field and removing it from the state's list of Entrys.

This is triggered by attribute [-ext] name.

def Lean.Meta.Ext.ExtTheorems.contains (d : ExtTheorems) (declName : Name) : Bool

Returns true if d contains theorem with name declName.

def Lean.Meta.Ext.isExtTheorem (declName : Name) : CoreM Bool

Returns true if declName is tagged with [ext] attribute.

def Lean.Meta.Ext.ExtTheorems.erase {m : Type → Type} [Monad m] [MonadError m] (d : ExtTheorems) (declName : Name) : m ExtTheorems

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.