Documentation

Lean.Elab.Tactic.Guard

The various guard_* tactics have similar matching specifiers for how equal expressions have to be to pass the tactic. This inductive gives the different specifiers that can be selected.

Instances For

    Converts a colon syntax into a MatchKind

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

      Converts a colonEq syntax into a MatchKind

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

        Converts a equal syntax into a MatchKind

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

          Elaborate a and b and then do the given equality test mk. We make sure to unify the types of a and b after elaboration so that when synthesizing pending metavariables we don't get the wrong instances due to default instances (for example, for nat literals).

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