Documentation

Mathlib.Tactic.WithoutCDot

The without_cdot() elaborator #

source
🔸 coverage
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.

Instances For
    source
    🔸 coverage
    def Lean.Elab.Term.withoutCDotImpl :
    Parser.Parser

    Implementation detail of withoutCDot

    Instances For
      source
      🔸 coverage
      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.

      Instances For