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.MVarId.generalize (mvarId : Lean.MVarId) (args : Array Lean.Meta.GeneralizeArg) : Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Telescopic generalize tactic. It can simultaneously generalize many terms. It uses kabstract to occurrences of the terms that need to be generalized.

Equations

• Lean.MVarId.generalize mvarId args = Lean.Meta.generalizeCore mvarId args

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

Telescopic generalize tactic. It can simultaneously generalize many terms. It uses kabstract to occurrences of the terms that need to be generalized.

Equations

• Lean.Meta.generalize mvarId args = Lean.Meta.generalizeCore mvarId args

def Lean.MVarId.generalizeHyp (mvarId : Lean.MVarId) (args : Array Lean.Meta.GeneralizeArg) (hyps : optParam (Array Lean.FVarId) #[]) (fvarSubst : optParam Lean.Meta.FVarSubst { map := ∅ }) : Lean.MetaM (Lean.Meta.FVarSubst × Array Lean.FVarId × Lean.MVarId)

Extension of generalize to support generalizing within specified hypotheses. The hyps array contains the list of hypotheses within which to look for occurrences of the generalizing expressions.

Equations

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