mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-27 10:41:08 +03:00
Don't collapse empty lines in 'lines'
This commit is contained in:
parent
8c9eec15a8
commit
ba9f14a18c
@ -71,10 +71,13 @@ unwords = pack . unwords' . map unpack
|
||||
||| lines' (unpack "\rA BC\nD\r\nE\n")
|
||||
||| ```
|
||||
lines' : List Char -> List (List Char)
|
||||
lines' s = case dropWhile isNL s of
|
||||
[] => []
|
||||
s' => let (w, s'') = break isNL s'
|
||||
in w :: lines' s''
|
||||
lines' [] = []
|
||||
lines' s = case break isNL s of
|
||||
(l, s') => l :: case s' of
|
||||
[] => []
|
||||
_ :: s'' => lines' (assert_smaller s s'')
|
||||
|
||||
|
||||
|
||||
||| Splits a string into a list of newline separated strings.
|
||||
|||
|
||||
|
Loading…
Reference in New Issue
Block a user