Implementation of the @[ext] attribute

Meta code for creating ext theorems

def Lean.Elab.Tactic.Ext.withExtHyps {α : Type} (struct : Name) (flat : Bool) (k : Array Expr → Expr → Expr → Array (Name × Expr) → MetaM α) : 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 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 : Name) (flat : Bool) : MetaM 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.

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

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

def Lean.Elab.Tactic.Ext.realizeExtTheorem (structName : Name) (flat : Bool) : Command.CommandElabM 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 : Name) : Command.CommandElabM 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.

Attribute

@[reducible, inline]

abbrev Lean.Elab.Tactic.Ext.extExtension : SimpleScopedEnvExtension Meta.Ext.ExtTheorem Meta.Ext.ExtTheorems

@[reducible, inline]

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

Implementation of ext tactic

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

Apply a single extensionality theorem to goal.

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

Apply a single extensionality theorem to the current goal.

def Lean.Elab.Tactic.Ext.tryIntros {m : Type → Type u_1} [Monad m] [MonadLiftT TermElabM m] (g : MVarId) (pats : List (TSyntax `rcasesPat)) (k : MVarId → List (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 TermElabM m] (g : MVarId) (pats : List (TSyntax `rcasesPat)) (k : MVarId → List (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.

def Lean.Elab.Tactic.Ext.withExtN {m : Type → Type u_1} [Monad m] [MonadLiftT TermElabM m] [MonadExcept Exception m] (g : MVarId) (pats : List (TSyntax `rcasesPat)) (k : MVarId → List (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.

def Lean.Elab.Tactic.Ext.extCore (g : MVarId) (pats : List (TSyntax `rcasesPat)) (depth : Nat := 100) (failIfUnchanged : Bool := true) : TermElabM (Nat × Array (MVarId × List (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 : Tactic