ppRoundtrip

Mathlib.Tactic.Linter.PPRoundtrip

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

Lean4

/-- The "ppRoundtrip" linter emits a warning when the syntax of a command differs substantially
from the pretty-printed version of itself.

The linter makes an effort to start the highlighting at the first difference.
However, it may not always be successful.
It also prints both the source code and the "expected code" in a 5-character radius from
the first difference.
-/
@[init initFn✝, ]
opaque ppRoundtrip : Lean.Option✝ Bool

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

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

Разделы

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

Аффилиация

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