def Std.Tactic.Ext.«commandDeclare_ext_theorems_for(Flat:=_)___» : Lean.ParserDescr

declare_ext_theorems_for A declares the extensionality theorems for the structure A.

Equations

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

structure Std.Tactic.Ext.ExtTheorem : Type

• declName : Lean.Name

  Declaration name of the extensionality theorem.

• priority : Nat

  Priority of the extensionality theorem.

• keys : Array (Lean.Meta.DiscrTree.Key true)

  Key in the discrimination tree.

Information about an extensionality theorem, stored in the environment extension.

instance Std.Tactic.Ext.instInhabitedExtTheorem : Inhabited Std.Tactic.Ext.ExtTheorem

Equations

• Std.Tactic.Ext.instInhabitedExtTheorem = { default := { declName := default, priority := default, keys := default } }

instance Std.Tactic.Ext.instReprExtTheorem : Repr Std.Tactic.Ext.ExtTheorem

Equations

• Std.Tactic.Ext.instReprExtTheorem = { reprPrec := Std.Tactic.Ext.reprExtTheorem✝ }

instance Std.Tactic.Ext.instBEqExtTheorem : BEq Std.Tactic.Ext.ExtTheorem

Equations

• Std.Tactic.Ext.instBEqExtTheorem = { beq := Std.Tactic.Ext.beqExtTheorem✝ }

instance Std.Tactic.Ext.instHashableExtTheorem : Hashable Std.Tactic.Ext.ExtTheorem

Equations

• Std.Tactic.Ext.instHashableExtTheorem = { hash := Std.Tactic.Ext.hashExtTheorem✝ }

structure Std.Tactic.Ext.ExtTheorems : Type

• tree : Lean.Meta.DiscrTree Std.Tactic.Ext.ExtTheorem true

  The tree of ext extensions.

• erased : Lean.PHashSet Lean.Name

  Erased exts.

The state of the ext extension environment

instance Std.Tactic.Ext.instInhabitedExtTheorems : Inhabited Std.Tactic.Ext.ExtTheorems

Equations

• Std.Tactic.Ext.instInhabitedExtTheorems = { default := { tree := default, erased := default } }

opaque Std.Tactic.Ext.extExtension : Lean.SimpleScopedEnvExtension Std.Tactic.Ext.ExtTheorem Std.Tactic.Ext.ExtTheorems

The environment extension to track @[ext] lemmas.

@[inline]

def Std.Tactic.Ext.getExtLemmas (ty : Lean.Expr) : Lean.MetaM (Array Std.Tactic.Ext.ExtTheorem)

Get the list of @[ext] lemmas 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 Std.Tactic.Ext.ExtTheorems.eraseCore (d : Std.Tactic.Ext.ExtTheorems) (declName : Lean.Name) : Std.Tactic.Ext.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.

Equations

• Std.Tactic.Ext.ExtTheorems.eraseCore d declName = { tree := d.tree, erased := Lean.PersistentHashSet.insert d.erased declName }

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

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

def Std.Tactic.Ext.ext : Lean.ParserDescr

Registers an extensionality lemma.

• When @[ext] is applied to a structure, it generates .ext and .ext_iff theorems and registers them for the ext tactic.

• When @[ext] is applied to a theorem, the theorem is registered for the ext tactic.

• You can use @[ext 9000] to specify a priority for the attribute.

• You can use the flag @[ext (flat := false)] to prevent flattening all fields of parent structures in the generated extensionality lemmas.

Equations

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