structure Lean.Meta.GeneralizeArg : Type

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

• expr : Expr
• xName? : Option Name
• hName? : Option Name

@[instance_reducible]

instance Lean.Meta.instInhabitedGeneralizeArg : Inhabited GeneralizeArg

Equations

• Lean.Meta.instInhabitedGeneralizeArg = { default := Lean.Meta.instInhabitedGeneralizeArg.default }

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

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

Equations

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

def Lean.MVarId.generalizeHyp (mvarId : MVarId) (args : Array Meta.GeneralizeArg) (hyps : Array FVarId := #[]) (fvarSubst : Meta.FVarSubst := { }) (transparency : Meta.TransparencyMode := Meta.TransparencyMode.instances) : MetaM (Meta.FVarSubst × Array FVarId × 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.