cdot

Mathlib.Tactic.Linter.Style

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.linter.style.cdot

Lean4

/-- The `cdot` linter flags uses of the "cdot" `·` that are achieved by typing a character
different from `·`.
For instance, a "plain" dot `.` is allowed syntax, but is flagged by the linter.
It also flags "isolated cdots", i.e. when the `·` is on its own line. -/
@[init initFn✝, ]
opaque cdot : Lean.Option✝ Bool

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru