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.

def Lean.Meta.Ext.instInhabitedExtTheorem.default : ExtTheorem

Equations

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

@[implicit_reducible]

instance Lean.Meta.Ext.instInhabitedExtTheorem : Inhabited ExtTheorem

Equations

• Lean.Meta.Ext.instInhabitedExtTheorem = { default := Lean.Meta.Ext.instInhabitedExtTheorem.default }

def Lean.Meta.Ext.instReprExtTheorem.repr : ExtTheorem → Nat → Format

Equations

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

@[implicit_reducible]

instance Lean.Meta.Ext.instReprExtTheorem : Repr ExtTheorem

Equations

• Lean.Meta.Ext.instReprExtTheorem = { reprPrec := Lean.Meta.Ext.instReprExtTheorem.repr }

@[implicit_reducible]

instance Lean.Meta.Ext.instBEqExtTheorem : BEq ExtTheorem

Equations

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

def Lean.Meta.Ext.instBEqExtTheorem.beq : ExtTheorem → ExtTheorem → Bool

Equations

• Lean.Meta.Ext.instBEqExtTheorem.beq { declName := a, priority := a_1, keys := a_2 } { declName := b, priority := b_1, keys := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Meta.Ext.instBEqExtTheorem.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Lean.Meta.Ext.instHashableExtTheorem : Hashable ExtTheorem

Equations

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

def Lean.Meta.Ext.instHashableExtTheorem.hash : ExtTheorem → UInt64

Equations

• Lean.Meta.Ext.instHashableExtTheorem.hash { declName := a, priority := a_1, keys := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

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].

@[implicit_reducible]

instance Lean.Meta.Ext.instInhabitedExtTheorems : Inhabited ExtTheorems

Equations

• Lean.Meta.Ext.instInhabitedExtTheorems = { default := Lean.Meta.Ext.instInhabitedExtTheorems.default }

def Lean.Meta.Ext.instInhabitedExtTheorems.default : 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.