Closed jsoo1 closed 5 years ago
I looked at the docs and packages are allowed to be named like "any valid idris identifier" (http://docs.idris-lang.org/en/latest/reference/packages.html). Does that mean the packages allowed should be expanded further?
May close #460
It looks like dashes are also supported since 1.2.0: https://github.com/idris-lang/Idris-dev/blob/master/CHANGELOG.md#packaging-updates
I looked at the docs and packages are allowed to be named like "any valid idris identifier" (http://docs.idris-lang.org/en/latest/reference/packages.html). Does that mean the packages allowed should be expanded further?
May close #460