Def Mathlib.Linter.Style.isDecideNative

Modification history

2025-06-04 15:50
Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean
feat: lint against using `native_decide` (#25297) …
Added Mathlib.Linter.Style.isDecideNativeView on Github →