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

doc: section/namespace/end (#3873)

Browse source 
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
This commit is contained in:
Sebastian Ullrich 2024-04-22 07:23:00 +02:00 • committed by GitHub
parent 41d310ab39
commit 7400a40116
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 26 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -208,10 +208,36 @@ def «structure» := leading_parser
"deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover ident skip) ", "
@[builtin_command_parser] def noncomputableSection := leading_parser
"noncomputable " >> "section" >> optional (ppSpace >> checkColGt >> ident)
/--
A `section`/`end` pair delimits the scope of `variable`, `open`, `set_option`, and `local` commands.
Sections can be nested. `section <id>` provides a label to the section that has to appear with the
matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the
end of the file.
-/
@[builtin_command_parser] def «section» := leading_parser
"section" >> optional (ppSpace >> checkColGt >> ident)
/--
`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside
the section:
* Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the
full name `Nat.seventeen`.
* Names introduced by `export` declarations are also prefixed by the identifier.
* All names starting with `<id>.` become available in the namespace without the prefix. These names
are preferred over names introduced by outer namespaces or `open`.
* Within a namespace, declarations can be `protected`, which excludes them from the effects of
opening the namespace.
As with `section`, namespaces can be nested and the scope of a namespace is terminated by a
corresponding `end <id>` or the end of the file.
`namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.
-/
@[builtin_command_parser] def «namespace» := leading_parser
"namespace " >> checkColGt >> ident
/--
`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
with `end <id>`.
-/
@[builtin_command_parser] def «end» := leading_parser
"end" >> optional (ppSpace >> checkColGt >> ident)
/-- Declares one or more typed variables, or modifies whether already-declared variables are