Lean App Tutorial, Part 7
This page assumes you've read Parts 1, 2, 3, 4, 5, and 6.
The end of Part 6 stated that you can use Lean namespaces just as easily as Lean sections. This tutorial page covers how to do so.
Namespaces
Recall the nicely organized theorem from the previous tutorial page.
We could do the same thing in a namespace rather than a section, if we wanted to. (We might want to in order to avoid filling the global namespace with too many identifiers, or to organize our code, or to prevent a clash with an existing theorem name, etc.)
It is a simple matter to change a section into a namespace, or vice versa.
- Right-click any text inside the Section bubble (but not inside any inner bubble).
- From the context menu, choose "Make this a namespace..."
- Enter a valid Lean identifier in the box that appears.
- Click OK and the section will become a namespace.
To rename the namespace, or convert it back to a section, follow the same procedure as above, but choosing the appropriate item from the context menu. They are named in the obvious way.
If the bubble shown above were a namespace, we could then access its contents outside the namespace using dot notation, as in any Lean code. See the following example.
So what?
Benefits
You can now organize your Lean code into namespaces in this app, just as you could in Lean. This is useful for the reasons stated above.
Missing pieces
The final missing piece is that this app does not seem to use any of the attractive symbols Lean uses, such as the blackboard bold N for natural numbers, and so on.
Let's see how to fix that in the final part of the tutorial.