From 7a65bde3e31bf2d46159bc1ba53519f636c4142a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 22 Apr 2024 09:18:17 +0200 Subject: [PATCH] doc: Command.set_option (#3872) Co-authored-by: Kim Morrison Co-authored-by: David Thrane Christiansen --- src/Lean/Parser/Command.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 5ac05daa14..bd6645ba2e 100644 --- a/src/Lean/Parser/Command.lean +++ b/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 ` sets the option `` to ``. 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 `` to list available options. + +`set_option in ` sets the option for just a single command: +``` +set_option pp.all true in +#check 1 + 1 +``` +Similarly, `set_option 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