Documentation

Lean.Meta.Tactic.Generalize

structure Lean.Meta.GeneralizeArg:

Type

expr : Lean.Expr
xName? : Option Lean.Name
hName? : Option Lean.Name

The generalize tactic takes arguments of the form h : e = x

instance Lean.Meta.instInhabitedGeneralizeArg:

Inhabited Lean.Meta.GeneralizeArg

Equations

Lean.Meta.instInhabitedGeneralizeArg = { default := { expr := default, xName? := default, hName? := default } }

def Lean.Meta.generalize (mvarId : Lean.MVarId) (args : Array Lean.Meta.GeneralizeArg) :

Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Equations

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

partial def Lean.Meta.generalize.go (args : Array Lean.Meta.GeneralizeArg) (target : Lean.Expr) (i : Nat) :

Lean.MetaM Lean.Expr

partial def Lean.Meta.generalize.go' (args : Array Lean.Meta.GeneralizeArg) (xs : Array Lean.Expr) (type : Lean.Expr) (i : Nat) :

Lean.MetaM (List Lean.Expr × Lean.Expr)