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

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

• declName : Lake.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

Equations

• Lean.Elab.Tactic.Ext.instReprExtTheorem = { reprPrec := Lean.Elab.Tactic.Ext.reprExtTheorem✝ }

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

Equations

• Lean.Elab.Tactic.Ext.instBEqExtTheorem = { beq := Lean.Elab.Tactic.Ext.beqExtTheorem✝ }

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

Equations

• Lean.Elab.Tactic.Ext.instHashableExtTheorem = { hash := Lean.Elab.Tactic.Ext.hashExtTheorem✝ }

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

  Erased exts via attribute [-ext].

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

Equations

• Lean.Elab.Tactic.Ext.instInhabitedExtTheorems = { default := { tree := default, erased := default } }

def Lean.Elab.Tactic.Ext.extExt.config : Lean.Meta.WhnfCoreConfig

Discrimation tree settings for the ext extension.

Equations

• Lean.Elab.Tactic.Ext.extExt.config = { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }

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.

Equations

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

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

• Lean.Elab.Tactic.Ext.ExtTheorems.eraseCore d 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 : Lake.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.

Equations

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

def Lean.Elab.Tactic.Ext.withExtHyps {α : Type} (struct : Lake.Name) (flat : Lean.Term) (k : Array Lean.Expr → Lean.Expr → Lean.Expr → Array (Lake.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 ty is x.field = y.field or HEq x.field y.field.

If flat parses to true, any fields inherited from parent structures are treated 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.elabExtType : Lean.Elab.Term.TermElab

Creates the type of the extensionality theorem for the given structure, elaborating to 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.elabExtIffType : Lean.Elab.Term.TermElab

Creates the type of the iff-variant of the extensionality theorem for the given structure, elaborating to x = y ↔ x.1 = y.1 ∧ x.2 = y.2, for example.

Equations

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

def Lean.Elab.Tactic.Ext.applyExtTheoremAt (goal : Lean.MVarId) : Lean.MetaM (List Lean.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 : Lean.Elab.Tactic.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 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.

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 (Lean.MVarId.intros g)) k __do_lift.snd []

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 : optParam Nat 1000000) (failIfUnchanged : optParam 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 : optParam Nat 1000000) (failIfUnchanged : optParam 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.)

Equations

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

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

Equations

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