Documentation

Batteries.Tactic.NoMatch

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

source
def Batteries.Tactic.matchWithDot :
Lean.ParserDescr

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

Both now support multiple discriminants.

Equations
    Instances For
      source
      def Batteries.Tactic.funDot :
      Lean.ParserDescr

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

      Equations
        Instances For
          source
          def Batteries.Tactic.lambdaDot :
          Lean.ParserDescr

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

          Equations
            Instances For
              source
              def Batteries.Tactic.«tacticMatch_,,With.» :
              Lean.ParserDescr

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

              Both now support multiple discriminants.

              Equations
                Instances For
                  source
                  def Batteries.Tactic.introDot :
                  Lean.ParserDescr

                  The syntax intro. is deprecated in favor of nofun.

                  Equations
                    Instances For