edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-25 13:54:55 +03:00
Code Issues Projects Releases Wiki Activity

Pack/unpack should be public export

Browse Source 
They're likely to be useful when manipulating strings in proofs.
This commit is contained in:
Edwin Brady 2019-08-01 11:17:38 +01:00
parent cb0ba4ef6a
commit 0b692e4379
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libs/prelude/Prelude.idr
View File

@ -861,7 +861,7 @@ strUncons : String -> Maybe (Char, String)
strUncons "" = Nothing strUncons "" = Nothing
strUncons str = Just (prim__strHead str, prim__strTail str) strUncons str = Just (prim__strHead str, prim__strTail str)
export public export
pack : List Char -> String pack : List Char -> String
pack [] = "" pack [] = ""
pack (x :: xs) = strCons x (pack xs) pack (x :: xs) = strCons x (pack xs)
@ -875,7 +875,7 @@ fastPack xs
toFArgs [] = [] toFArgs [] = []
toFArgs (x :: xs) = x :: toFArgs xs toFArgs (x :: xs) = x :: toFArgs xs
export public export
unpack : String -> List Char unpack : String -> List Char
unpack str = unpack' 0 (prim__cast_IntegerInt (natToInteger (length str))) str unpack str = unpack' 0 (prim__cast_IntegerInt (natToInteger (length str))) str
where where