Def Mathlib.Linter.Style.nameCheck.doubleUnderscore

Modification history

2025-07-01 00:55

Mathlib/Tactic/Linter/Style.lean

chore: bump toolchain to v4.22.0-rc2 (#26564) …

Added Mathlib.Linter.Style.nameCheck.doubleUnderscore View on Github →