You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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 andMyPackage
for packages.The text was updated successfully, but these errors were encountered: