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 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 : 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