Documentation

Std.Tactic.Ext

def Std.Tactic.Ext.withExtHyps {α : Type} (struct : Lean.Name) (k : Array Lean.Expr → Lean.Expr → Lean.Expr → Array (Lean.Name × Lean.Expr) → Lean.MetaM α) :

Constructs the hypotheses for the extensionality lemma. 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.

Equations

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

def Std.Tactic.Ext.«termExt_type%_» :

Lean.ParserDescr

Creates the type of the extensionality lemma 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 Std.Tactic.Ext.mkIff (p : Lean.Expr) (q : Lean.Expr) :

Make an Iff application.

Equations

Std.Tactic.Ext.mkIff p q = Lean.mkApp2 (Lean.mkConst `Iff) p q

def Std.Tactic.Ext.mkAndN :

List Lean.Expr → Lean.Expr

Make an n-ary And application. mkAndN [] returns True.

Equations

Std.Tactic.Ext.mkAndN [] = Lean.mkConst `True
Std.Tactic.Ext.mkAndN [p] = p
Std.Tactic.Ext.mkAndN (p :: ps) = Lean.mkAnd p (Std.Tactic.Ext.mkAndN ps)

def Std.Tactic.Ext.«termExt_iff_type%_» :

Lean.ParserDescr

Creates the type of the iff-variant of the extensionality lemma 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 Std.Tactic.Ext.applyExtLemma (goal : Lean.MVarId) :

Lean.MetaM (List Lean.MVarId)

Apply a single extensionality lemma to goal.

Equations

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

def Std.Tactic.Ext.tacticApply_ext_lemma :

Lean.ParserDescr

Apply a single extensionality lemma to the current goal.

Equations

Std.Tactic.Ext.tacticApply_ext_lemma = Lean.ParserDescr.node `Std.Tactic.Ext.tacticApply_ext_lemma 1024 (Lean.ParserDescr.nonReservedSymbol "apply_ext_lemma" false)

def Std.Tactic.Ext.tryIntros {m : Type → Type u_1} [inst : Monad m] [inst : MonadLiftT Lean.Elab.TermElabM m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m Unit) :

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.

def Std.Tactic.Ext.withExt1 {m : Type → Type u_1} [inst : Monad m] [inst : MonadLiftT Lean.Elab.TermElabM m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m Unit) :

Applies a single extensionality lemma, 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 Std.Tactic.Ext.withExtN {m : Type → Type u_1} [inst : Monad m] [inst : MonadLiftT Lean.Elab.TermElabM m] [inst : MonadExcept Lean.Exception m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m Unit) (depth : optParam Nat 1000000) (failIfUnchanged : optParam Bool true) :

Applies a extensionality lemmas 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.
Std.Tactic.Ext.withExtN g pats k 0 failIfUnchanged = k g pats

def Std.Tactic.Ext.extCore (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (depth : optParam Nat 1000000) (failIfUnchanged : optParam Bool true) :

Lean.Elab.TermElabM (Array (Lean.MVarId × List (Lean.TSyntax `rcasesPat)))

Apply extensionality lemmas as much as possible, using pats to introduce the variables in extensionality lemmas like funext. Returns a list of subgoals, and the unconsumed patterns in each of those subgoals.

Equations

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

def Std.Tactic.Ext.«tacticExt___:_» :

Lean.ParserDescr

ext pat*: Apply extensionality lemmas as much as possible, using pat* to introduce the variables in extensionality lemmas like funext.
ext: introduce anonymous variables whenever needed.

Equations

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

def Std.Tactic.Ext.tacticExt1___ :

Lean.ParserDescr

ext1 pat* is like ext pat* except it only applies one extensionality lemma instead of recursing as much as possible.

Equations

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

def Std.Tactic.Ext.tacticExt1?___ :

Lean.ParserDescr

ext1? pat* is like ext1 pat* but gives a suggestion on what pattern to use

Equations

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

def Std.Tactic.Ext.«tacticExt?___:_» :

Lean.ParserDescr

ext? pat* is like ext pat* but gives a suggestion on what pattern to use

Equations

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

theorem PUnit.ext (x : PUnit) (y : PUnit) :

x = y

theorem Unit.ext (x : Unit) (y : Unit) :

x = y