Commit 2025-06-04 15:50 fbce7ad3
View on Github →feat: lint against using native_decide (#25297)
Mathlib disallows this (as it depends on the entire Lean compiler, and not just the kernel).
The lean4checker job would already detect this (as using native_decide uses the ofReduceBool axiom): the purpose of this linter is to provide quick user feedback.
Zulip discussion