Telescopic generalize
tactic. It can simultaneously generalize many terms.
It uses kabstract
to occurrences of the terms that need to be generalized.
Instances For
@[deprecated Lean.MVarId.generalize]
Telescopic generalize
tactic. It can simultaneously generalize many terms.
It uses kabstract
to occurrences of the terms that need to be generalized.
Instances For
def
Lean.MVarId.generalizeHyp
(mvarId : Lean.MVarId)
(args : Array Lean.Meta.GeneralizeArg)
(hyps : optParam (Array Lean.FVarId) #[])
(fvarSubst : optParam Lean.Meta.FVarSubst { map := ∅ })
:
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.