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

[ performance ] add fastUnlines to base

Browse Source
This commit is contained in:
stefan-hoeck 2021-03-26 11:45:07 +01:00 committed by G. Allais
parent 028f82f70c
commit 6824111fd8
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libs/base/Data/String.idr
View File

@ -37,6 +37,11 @@ fastUnpack : String -> List Char
export export
fastConcat : List String -> String fastConcat : List String -> String
-- This uses fastConcat internally so it won't compute at compile time.
export
fastUnlines : List String -> String
fastUnlines = fastConcat . intersperse "\n"
-- This is a deprecated alias for fastConcat for backwards compatibility -- This is a deprecated alias for fastConcat for backwards compatibility
-- (unfortunately, we don't have %deprecated yet). -- (unfortunately, we don't have %deprecated yet).
export export