idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 09:12:34 +03:00
Code Issues Projects Releases Wiki Activity

Allowing for an empty package name.

Browse Source
This commit is contained in:
Matthew-Mosior 2024-07-26 14:20:51 -04:00
parent 8e24f12e60
commit ba560de6c3
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Idris/Package/Init.idr
View File

@ -112,6 +112,6 @@ interactive = do
True => isIdentTrailing xs True => isIdentTrailing xs
checkPackageName : List Char -> Bool checkPackageName : List Char -> Bool
checkPackageName [] = False checkPackageName [] = True
checkPackageName (x::xs) = isIdentStart x && checkPackageName (x::xs) = isIdentStart x &&
isIdentTrailing xs isIdentTrailing xs