Documentation

Lean.Meta.Tactic.Subst

Instances For

    Given h : HEq α a α b in the given goal, produce a new goal where h : Eq α a b. If h is not of the give form, then just return (h, mvarId)

    Instances For

      Give h : Eq α a b, try to apply substCore

      Instances For

        Try to find an equation of the form heq : h = rhs or heq : lhs = h

        Instances For
          Instances For
            Instances For
              Instances For