source
structure Lean.Meta.GeneralizeArg :
Type

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

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

Instances For

source
def Lean.Meta.instInhabitedGeneralizeArg.default :
GeneralizeArg
Equations

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

Instances For

source
instance Lean.Meta.instInhabitedGeneralizeArg :
Inhabited GeneralizeArg
Equations

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

source
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

Instances For

source
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.

Instances For