doc: Command.set_option (#3872)

Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

src/Lean/Parser/Command.lean

@@ -419,6 +419,21 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
+/--
+`set_option <id> <value>` sets the option `<id>` to `<value>`. Depending on the type of the option,
+the value can be `true`, `false`, a string, or a numeral. Options are used to configure behavior of
+Lean as well as user-defined extensions. The setting is active until the end of the current `section`
+or `namespace` or the end of the file.
+Auto-completion is available for `<id>` to list available options.
+
+`set_option <id> <value> in <command>` sets the option for just a single command:
+```
+set_option pp.all true in
+#check 1 + 1
+```
+Similarly, `set_option <id> <value> in` can also be used inside terms and tactics to set an option
+only in a single term or tactic.
+-/
 @[builtin_command_parser] def «set_option»   := leading_parser
   "set_option " >> identWithPartialTrailingDot >> ppSpace >> optionValue
 def eraseAttr := leading_parser