Documentation

Lean.Meta.Tactic.Subst

Equations
  • One or more equations did not get rendered due to their size.
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)

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Given x, try to find an equation of the form heq : x = rhs or heq : lhs = x, and runs substCore on it. Throws an exception if no such equation is found.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Given x, try to find an equation of the form heq : x = rhs or heq : lhs = x, and runs substCore on it. Returns none if no such equation is found, or if substCore fails.

          Equations
          Instances For
            Equations
            Instances For
              Equations
              Instances For
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For