Def Mathlib.Linter.Style.isDecideNative

Modification history

2026-08-31 16:15
Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean
refactor(Tactic/Linter): rename and generalize `linter.style.nativeDecide` to `linter.style.native` (#43194) …
Deleted Mathlib.Linter.Style.isDecideNativeView on Github →
2025-06-04 15:50
Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean
feat: lint against using `native_decide` (#25297) …
Added Mathlib.Linter.Style.isDecideNativeView on Github →