ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-11 08:55:23 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #3734 from mheinzel/lib-documentation-typos

Browse Source 
Fix typos etc. in String docs
This commit is contained in:
Ahmad Salim Al-Sibahi 2017-04-04 09:29:36 +02:00 committed by GitHub
commit e019840290
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libs/prelude/Prelude/Strings.idr
View File

@ -37,7 +37,7 @@ foldl1 f (x::xs) = foldl f x xs
(++) = prim__concat
||| A preallocated buffer for building a String. This allows a function (in IO)
||| to allocate enough space for a stirng which will be build from smaller
||| to allocate enough space for a string which will be built from smaller
||| pieces without having to allocate at every step.
||| To build a string using a `StringBuffer`, see `newStringBuffer`,
||| `addToStringBuffer` and `getStringFromBuffer`.
@ -247,7 +247,7 @@ break p = span (not . p)
split : (Char -> Bool) -> String -> List String
split p xs = map pack (split p (unpack xs))
||| Removes whitespace (determined with 'isSpace') from
||| Removes whitespace (determined by 'isSpace') from
||| the start of the string.
|||
||| ```idris example
@ -262,7 +262,7 @@ ltrim xs with (strM xs)
ltrim (strCons x xs) | StrCons _ _
= if (isSpace x) then assert_total (ltrim xs) else (strCons x xs)
||| Removes whitespace (determined with 'isSpace') from
||| Removes whitespace (determined by 'isSpace') from
||| the start and end of the string.
|||
||| ```idris example
@ -371,7 +371,7 @@ toLower x with (strM x)
||| Uppercases all characters in the string.
|||
||| ```idris example
||| toLower "aBc12!"
||| toUpper "aBc12!"
||| ```
toUpper : String -> String
toUpper x with (strM x)