From 61ee3b2711022136a0edf8febd115f3880fcbab5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Oct 2025 15:57:47 -0700 Subject: [PATCH] feat: expose `optionValue` parser (#10839) This PR exposes the `optionValue` parser used to implement the `set_option` notation. --- src/Lean/Parser/Command.lean | 17 +++++++++-------- stage0/src/stdlib_flags.h | 1 + 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index ced5a06697..57abbf5eee 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -909,14 +909,15 @@ abbrev declModifiersT := declModifiers true builtin_initialize register_parser_alias (kind := ``declModifiers) "declModifiers" declModifiersF register_parser_alias (kind := ``declModifiers) "nestedDeclModifiers" declModifiersT - register_parser_alias declId - register_parser_alias declSig - register_parser_alias declVal - register_parser_alias optDeclSig - register_parser_alias openDecl - register_parser_alias docComment - register_parser_alias plainDocComment - register_parser_alias visibility + register_parser_alias declId + register_parser_alias declSig + register_parser_alias declVal + register_parser_alias optDeclSig + register_parser_alias openDecl + register_parser_alias docComment + register_parser_alias plainDocComment + register_parser_alias visibility + register_parser_alias "optionValue" Command.optionValue /-- Registers an error explanation. diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..ad491b0de1 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,3 +1,4 @@ +// update me! #include "util/options.h" namespace lean {