Documentation

Batteries.Tactic.NoMatch

Deprecation warnings for match ⋯ with., fun., λ., and intro..

The syntax match ⋯ with. has been deprecated in favor of nomatch ⋯.

Both now support multiple discriminants.

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

    The syntax fun. has been deprecated in favor of nofun.

    Equations
    Instances For

      The syntax λ. has been deprecated in favor of nofun.

      Equations
      Instances For

        The syntax match ⋯ with. has been deprecated in favor of nomatch ⋯.

        Both now support multiple discriminants.

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

          The syntax intro. is deprecated in favor of nofun.

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