Currently Inigo allows you to choose invalid namespaces or package names. We should restrict these to names that are compatible with Idris (or allow you to specify a package name that differs from the module names). For the time-being, the solution is to simply use a name like MyNamespace for namespaces and MyPackage for packages.
Currently Inigo allows you to choose invalid namespaces or package names. We should restrict these to names that are compatible with Idris (or allow you to specify a package name that differs from the module names). For the time-being, the solution is to simply use a name like
MyNamespacefor namespaces andMyPackagefor packages.