The without_cdot() elaborator

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

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

def Lean.Elab.Term.withoutCDotImpl : Parser.Parser

Implementation detail of withoutCDot

Equations

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

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

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