Using config vs optConfig in language documentation

Stream: general

[Michael Rothgang]

I just stumbled upon this blob of the language reference --- using "old" config syntax. These days, I'd rather wrote simp +contextualthan simp (config := {contextual := true}). What are opinions here, is a PR changing this welcome?

[Robin Arnez]

Yeah this should probably show more modern syntax

[Robin Arnez]

For reference, here is the source: https://github.com/leanprover/lean4/blob/ff130a25a21dcd3b3d2c9ae6fcbd21def22287ee/src/Init/MetaTypes.lean#L141-L146

[Michael Rothgang]

Thanks! PR at lean4#9174