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

fix: namespaces.md

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-20 07:56:53 -08:00
parent eba78e2d83
commit 40ab77288d
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/namespaces.md
View file

@ -100,9 +100,9 @@ end Foo
```
Like sections, nested namespaces have to be closed in the order they are opened.
Also, a namespace cannot be declared within a section; namespaces have to live on the outer levels.
Namespaces and sections serve different purposes: namespaces organize data and sections declare variables for insertion in definitions.
Sections are also useful for delimiting the scope of commands such as ``set_option`` and ``open``.
In many respects, however, a ``namespace ... end`` block behaves the same as a ``section ... end`` block.
In particular, if you use the ``variable`` command within a namespace, its scope is limited to the namespace.
Similarly, if you use an ``open`` command within a namespace, its effects disappear when the namespace is closed.