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.
We want Lean's namespaces for the following reason:
#[1,2,3].map (\x -> x + 1)The way it should be implemented: