Implementation of the @[ext] attribute

Meta code for creating ext theorems

Attribute

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