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

Equations

• Lean.Meta.Ext.instInhabitedExtTheorem = { default := { declName := default, priority := default, keys := default } }

instance Lean.Meta.Ext.instReprExtTheorem : Repr ExtTheorem

Equations

• Lean.Meta.Ext.instReprExtTheorem = { reprPrec := Lean.Meta.Ext.reprExtTheorem✝ }

instance Lean.Meta.Ext.instBEqExtTheorem : BEq ExtTheorem

Equations

• Lean.Meta.Ext.instBEqExtTheorem = { beq := Lean.Meta.Ext.beqExtTheorem✝ }

instance Lean.Meta.Ext.instHashableExtTheorem : Hashable ExtTheorem

Equations

• Lean.Meta.Ext.instHashableExtTheorem = { hash := Lean.Meta.Ext.hashExtTheorem✝ }

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

Equations

• Lean.Meta.Ext.instInhabitedExtTheorems = { default := { tree := default, erased := default } }

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• d.eraseCore declName = { tree := d.tree, erased := Lean.PersistentHashSet.insert d.erased declName }

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

Returns true if d contains theorem with name declName.

Equations

• d.contains declName = ((d.tree.containsValueP fun (x : Lean.Meta.Ext.ExtTheorem) => x.declName == declName) && !Lean.PersistentHashSet.contains d.erased declName)

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

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.