Documentation

Mathlib.Tactic.WithoutCDot

The without_cdot() elaborator #

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

      Implementation detail of withoutCDot

      Equations
        Instances For

          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