From a7c982204e9b8808eec72909892e0ea5f35a391c Mon Sep 17 00:00:00 2001 From: grunweg Date: Thu, 3 Jul 2025 16:16:37 +0200 Subject: [PATCH] doc: use modern configuration syntax in the Simp.Config documentation (#9174) The new config syntax is preferred for new code: change the documentation to use it. This was [discussed on zulip](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Using.20config.20vs.20optConfig.20in.20language.20documentation/with/526948836). --- src/Init/MetaTypes.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index a410360e09..c19612b500 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -140,7 +140,7 @@ def defaultMaxSteps := 100000 /-- The configuration for `simp`. -Passed to `simp` using, for example, the `simp (config := {contextual := true})` syntax. +Passed to `simp` using, for example, the `simp +contextual` or `simp (maxSteps := 100000)` syntax. See also `Lean.Meta.Simp.neutralConfig` and `Lean.Meta.DSimp.Config`. -/