Namespaces

[alcides]

We want Lean's namespaces for the following reason:

• We want to group functions that we can import for synthesis (or that we want to ignore as a whole).
• We want to be able to define List.map, and then if the name of the type (constructor) is the same of a namespace, you can do: #[1,2,3].map (\x -> x + 1)

The way it should be implemented:

• Add support for using the "." in the identifiers of function definitions.
• Add support for using "." in variables.
• Verify that TypingContext and EvaluationContexts have the right names.