5 lines
98 B
Lean4
5 lines
98 B
Lean4
import Mathlib.Lean.Meta.Simp
|
|
|
|
/-- Simp set for `functor_norm` -/
|
|
register_simp_attr MyNat_decide
|