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
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.withoutCDotImpl :
Parser.Parser

Implementation detail of withoutCDot

Equations
  • One or more equations did not get rendered due to their size.
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
  • One or more equations did not get rendered due to their size.