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.

Equations

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

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.

Equations

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

def Lean.Elab.Tactic.Ext.mkExtIffType (extThmName : Name) : MetaM 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 : 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.

Equations

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

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.

Equations

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

Attribute

@[reducible, inline]

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

Equations

• Lean.Elab.Tactic.Ext.extExtension = Lean.Meta.Ext.extExtension

@[reducible, inline]

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

Equations

• Lean.Elab.Tactic.Ext.getExtTheorems = Lean.Meta.Ext.getExtTheorems

Implementation of ext tactic

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

Apply a single extensionality theorem to goal.

Equations

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

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

Apply a single extensionality theorem to the current goal.

Equations

• Lean.Elab.Tactic.Ext.evalApplyExtTheorem x✝ = Lean.Elab.Tactic.liftMetaTactic Lean.Elab.Tactic.Ext.applyExtTheoremAt

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.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.Ext.tryIntros g [] k = do let __do_lift ← liftM (liftM g.intros) k __do_lift.snd []

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.

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

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

Equations

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

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

Equations

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