Commit 2024-02-14 08:30 bfaf1a5e
View on Github →feat: simp config opts in norm_num (#7112)
This adds support for norm_num (config := ...), which just forwards the config args to simp. The case of {decide := false} came up in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Prove.20decidable.20statement.20by.20evaluation/near/390390131 .