Documentation

Mathlib.Tactic.WithoutCDot

The without_cdot() elaborator #

source
def Lean.Elab.Term.withoutCDot :
Parser.Parser

A set of parentheses, supporting type ascriptions, which does not process ·.

Primarily, this is useful when quoting user-provided syntax inside parentheses, as it prevents ·s from the caller being interpreted in the context of ()s from the macro.

Equations
    Instances For
      source
      def Lean.Elab.Term.withoutCDotImpl :
      Parser.Parser

      Implementation detail of withoutCDot

      Equations
        Instances For
          source
          def Lean.Elab.Term.elabWithoutCDot :
          TermElab

          A set of parentheses, supporting type ascriptions, which does not process ·.

          Primarily, this is useful when quoting user-provided syntax inside parentheses, as it prevents ·s from the caller being interpreted in the context of ()s from the macro.

          Equations
            Instances For