Documentation

Batteries.Tactic.NoMatch

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

source
🔸 coverage
def Batteries.Tactic.matchWithDot :
Lean.ParserDescr

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
    source
    🔸 coverage
    def Batteries.Tactic.funDot :
    Lean.ParserDescr

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

    Equations
    • Batteries.Tactic.funDot = Lean.ParserDescr.node `Batteries.Tactic.funDot 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "fun") (Lean.ParserDescr.symbol "."))
    Instances For
      source
      🔸 coverage
      def Batteries.Tactic.lambdaDot :
      Lean.ParserDescr

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

      Equations
      • Batteries.Tactic.lambdaDot = Lean.ParserDescr.node `Batteries.Tactic.lambdaDot 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "λ") (Lean.ParserDescr.symbol "."))
      Instances For
        source
        🔸 coverage
        def Batteries.Tactic.«tacticMatch_,,With.» :
        Lean.ParserDescr

        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
          source
          🔸 coverage
          def Batteries.Tactic.introDot :
          Lean.ParserDescr

          The syntax intro. is deprecated in favor of nofun.

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