max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: expose optionValue parser (#10839)

Browse source 
This PR exposes the `optionValue` parser used to implement the
`set_option` notation.
This commit is contained in:
Leonardo de Moura 2025-10-19 15:57:47 -07:00 • committed by GitHub
parent 206eb73cd9
commit 61ee3b2711
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Lean/Parser/Command.lean
View file

@ -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.

1
stage0/src/stdlib_flags.h
View file

@ -1,3 +1,4 @@
// update me!
#include "util/options.h"
namespace lean {