Implementation of the @[ext] attribute

Meta code for creating ext theorems

def Lean.Elab.Tactic.Ext.withExtHyps {α : Type} (struct : Lean.Name) (flat : Bool) (k : Array Lean.Expr → Lean.Expr → Lean.Expr → Array (Lean.Name × Lean.Expr) → Lean.MetaM α) : Lean.MetaM α

Constructs the hypotheses for the structure extensionality theorem that states that two structures are equal if their fields are equal.

Calls the continuation k with the list of parameters to the structure, two structure variables x and y, and a list of pairs (field, ty) where each ty is of the form x.field = y.field or HEq x.field y.field.

If flat parses to true, any fields inherited from parent structures are treated as fields of the given structure type. If it is false, then the behind-the-scenes encoding of inherited fields is visible in the extensionality lemma.

def Lean.Elab.Tactic.Ext.mkExtType (structName : Lean.Name) (flat : Bool) : Lean.MetaM Lean.Expr

Creates the type of the extensionality theorem for the given structure, returning ∀ {x y : Struct}, x.1 = y.1 → x.2 = y.2 → x = y, for example.

Equations

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

def Lean.Elab.Tactic.Ext.mkExtIffType (extThmName : Lean.Name) : Lean.MetaM Lean.Expr

Derives the type of the iff form of an ext theorem.

Equations

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

def Lean.Elab.Tactic.Ext.realizeExtTheorem (structName : Lean.Name) (flat : Bool) : Lean.Elab.Command.CommandElabM Lean.Name

Ensures that the given structure has an ext theorem, without validating any pre-existing theorems. Returns the name of the ext theorem.

See Lean.Elab.Tactic.Ext.withExtHyps for an explanation of the flat argument.

def Lean.Elab.Tactic.Ext.realizeExtIffTheorem (extName : Lean.Name) : Lean.Elab.Command.CommandElabM Lean.Name

Given an 'ext' theorem, ensures that there is an iff version of the theorem (if possible), without validating any pre-existing theorems. Returns the name of the 'ext_iff' theorem.

Equations

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

Attribute

structure Lean.Elab.Tactic.Ext.ExtTheorem : Type

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

• declName : Lean.Name

  Declaration name of the extensionality theorem.

• priority : Nat

  Priority of the extensionality theorem.

• keys : Array Lean.Meta.DiscrTree.Key

  Key in the discrimination tree, for the type in which the extensionality theorem holds.

instance Lean.Elab.Tactic.Ext.instInhabitedExtTheorem : Inhabited Lean.Elab.Tactic.Ext.ExtTheorem

Equations

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

instance Lean.Elab.Tactic.Ext.instReprExtTheorem : Repr Lean.Elab.Tactic.Ext.ExtTheorem

instance Lean.Elab.Tactic.Ext.instBEqExtTheorem : BEq Lean.Elab.Tactic.Ext.ExtTheorem

instance Lean.Elab.Tactic.Ext.instHashableExtTheorem : Hashable Lean.Elab.Tactic.Ext.ExtTheorem

structure Lean.Elab.Tactic.Ext.ExtTheorems : Type

The state of the ext extension environment

• tree : Lean.Meta.DiscrTree Lean.Elab.Tactic.Ext.ExtTheorem

  The tree of ext extensions.

• erased : Lean.PHashSet Lean.Name

  Erased exts via attribute [-ext].

instance Lean.Elab.Tactic.Ext.instInhabitedExtTheorems : Inhabited Lean.Elab.Tactic.Ext.ExtTheorems

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

The environment extension to track @[ext] theorems.

@[inline]

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

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

def Lean.Elab.Tactic.Ext.ExtTheorems.eraseCore (d : Lean.Elab.Tactic.Ext.ExtTheorems) (declName : Lean.Name) : Lean.Elab.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.

This is triggered by attribute [-ext] name.

Equations

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

def Lean.Elab.Tactic.Ext.ExtTheorems.erase {m : Type → Type} [Monad m] [Lean.MonadError m] (d : Lean.Elab.Tactic.Ext.ExtTheorems) (declName : Lean.Name) : m Lean.Elab.Tactic.Ext.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.

Implementation of ext tactic

def Lean.Elab.Tactic.Ext.applyExtTheoremAt (goal : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Apply a single extensionality theorem to goal.

def Lean.Elab.Tactic.Ext.evalApplyExtTheorem : Lean.Elab.Tactic.Tactic

Apply a single extensionality theorem to the current goal.

def Lean.Elab.Tactic.Ext.tryIntros {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.Elab.TermElabM m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m Nat) : m Nat

Postprocessor for withExt which runs rintro with the given patterns when the target is a pi type.

def Lean.Elab.Tactic.Ext.withExt1 {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.Elab.TermElabM m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m Nat) : m Nat

Applies a single extensionality theorem, using pats to introduce variables in the result. Runs continuation k on each subgoal.

Equations

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

def Lean.Elab.Tactic.Ext.withExtN {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.Elab.TermElabM m] [MonadExcept Lean.Exception m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m Nat) (depth : Nat := 100) (failIfUnchanged : Bool := true) : m Nat

Applies extensionality theorems recursively, using pats to introduce variables in the result. Runs continuation k on each subgoal.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.Ext.withExtN g pats k 0 failIfUnchanged = k g pats

def Lean.Elab.Tactic.Ext.extCore (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (depth : Nat := 100) (failIfUnchanged : Bool := true) : Lean.Elab.TermElabM (Nat × Array (Lean.MVarId × List (Lean.TSyntax `rcasesPat)))

Apply extensionality theorems as much as possible, using pats to introduce the variables in extensionality theorems like funext. Returns a list of subgoals.

This is built on top of withExtN, running in TermElabM to build the list of new subgoals. (And, for each goal, the patterns consumed.)

def Lean.Elab.Tactic.Ext.evalExt : Lean.Elab.Tactic.Tactic

Equations

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