Documentation

Lean.Meta.Tactic.Generalize

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

Instances For
    Equations

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

    Equations
    Instances For

      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