edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-29 07:44:45 +03:00
Code Issues Projects Releases Wiki Activity

Add strIndex and strTail

Browse Source
This commit is contained in:
Edwin Brady 2020-01-31 23:06:08 +00:00
parent 886b6aae7f
commit 284a3ded69
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libs/base/Data/Strings.idr
View File

@ -165,3 +165,11 @@ toUpper str = pack (map toUpper (unpack str))
export
toLower : String -> String
toLower str = pack (map toLower (unpack str))
export
strIndex : String -> Int -> Char
strIndex = prim__strIndex
export
strTail : String -> String
strTail = prim__strTail