@@ -17,8 +17,9 @@ import Decidable.Equality
1717
1818||| Appends two strings together.
1919|||
20−||| Idris> "AB" ++ "C"
21−||| "ABC" : String
20+||| ```idris example
21+||| "AB" ++ "C"
22+||| ```
2223(++) : String -> String -> String
2324(++) = prim__concat
2425
@@ -26,8 +27,9 @@ import Decidable.Equality
2627|||
2728||| Doesn't work for empty strings.
2829|||
29−||| Idris> strHead "A"
30−||| 'A' : Char
30+||| ```idris example
31+||| strHead "A"
32+||| ```
3133partial
3234strHead : String -> Char
3335strHead = prim__strHead
@@ -36,20 +38,24 @@ strHead = prim__strHead
3638|||
3739||| Doesn't work for empty strings.
3840|||
39−||| Idris> strTail "AB"
40−||| "B" : String
41−||| Idris> strTail "A"
42−||| "" : String
41+||| ```idris example
42+||| strTail "AB"
43+||| ```
44+||| ```idris example
45+||| strTail "A"
46+||| ```
4347partial
4448strTail : String -> String
4549strTail = prim__strTail
4650
4751||| Adds a character to the front of the specified string.
4852|||
49−||| Idris> strCons 'A' "B"
50−||| "AB" : String
51−||| Idris> strCons 'A' ""
52−||| "A" : String
53+||| ```idris example
54+||| strCons 'A' "B"
55+||| ```
56+||| ```idris example
57+||| strCons 'A' ""
58+||| ```
5359strCons : Char -> String -> String
5460strCons = prim__strCons
5561
@@ -57,18 +63,21 @@ strCons = prim__strCons
5763|||
5864||| Precondition: '0 < i < length s' for 'strIndex s i'.
5965|||
60−||| Idris> strIndex "AB" 1
61−||| 'B' : Char
66+||| ```idris example
67+||| strIndex "AB" 1
68+||| ```
6269partial
6370strIndex : String -> Int -> Char
6471strIndex = prim__strIndex
6572
6673||| Reverses the elements within a String.
6774|||
68−||| Idris> reverse "ABC"
69−||| "CBA" : String
70−||| Idris> reverse ""
71−||| "" : String
75+||| ```idris example
76+||| reverse "ABC"
77+||| ```
78+||| ```idris example
79+||| reverse ""
80+||| ```
7281reverse : String -> String
7382reverse = prim__strRev
7483
@@ -103,8 +112,9 @@ strM x with (decEq (not (x == "")) True)
103112
104113||| Turns a string into a list of characters.
105114|||
106−||| Idris> unpack "ABC"
107−||| ['A', 'B', 'C'] : List Char
115+||| ```idris example
116+||| unpack "ABC"
117+||| ```
108118unpack : String -> List Char
109119unpack s with (strM s)
110120 unpack "" | StrNil = []
@@ -116,8 +126,9 @@ pack = foldr strCons ""
116126
117127||| Creates a string of a single character.
118128|||
119−||| Idris> singleton 'A'
120−||| "A" : String
129+||| ```idris example
130+||| singleton 'A'
131+||| ```
121132singleton : Char -> String
122133singleton c = strCons c ""
123134
@@ -139,10 +150,12 @@ instance Monoid String where
139150||| Splits the string into a part before the predicate
140151||| returns False and the rest of the string.
141152|||
142−||| Idris> span (/= 'C') "ABCD"
143−||| ("AB", "CD") : (String, String)
144−||| Idris> span (/= 'C') "EFGH"
145−||| ("EFGH", "") : (String, String)
153+||| ```idris example
154+||| span (/= 'C') "ABCD"
155+||| ```
156+||| ```idris example
157+||| span (/= 'C') "EFGH"
158+||| ```
146159span : (Char -> Bool) -> String -> (String, String)
147160span p xs with (strM xs)
148161 span p "" | StrNil = ("", "")
@@ -154,28 +167,33 @@ span p xs with (strM xs)
154167||| Splits the string into a part before the predicate
155168||| returns True and the rest of the string.
156169|||
157−||| Idris> break (== 'C') "ABCD"
158−||| ("AB", "CD") : (String, String)
159−||| Idris> break (== 'C') "EFGH"
160−||| ("EFGH", "") : (String, String)
170+||| ```idris example
171+||| break (== 'C') "ABCD"
172+||| ```
173+||| ```idris example
174+||| break (== 'C') "EFGH"
175+||| ```
161176break : (Char -> Bool) -> String -> (String, String)
162177break p = span (not . p)
163178
164179||| Splits the string into parts with the predicate
165180||| indicating separator characters.
166181|||
167−||| Idris> split (== '.') ".AB.C..D"
168−||| ["", "AB", "C", "", "D"] : List String
182+||| ```idris example
183+||| split (== '.') ".AB.C..D"
184+||| ```
169185split : (Char -> Bool) -> String -> List String
170186split p xs = map pack (split p (unpack xs))
171187
172188||| Removes whitespace (determined with 'isSpace') from
173189||| the start of the string.
174190|||
175−||| Idris> ltrim " A\nB"
176−||| "A\nB" : String
177−||| Idris> ltrim " \nAB"
178−||| "AB" : String
191+||| ```idris example
192+||| ltrim " A\nB"
193+||| ```
194+||| ```idris example
195+||| ltrim " \nAB"
196+||| ```
179197ltrim : String -> String
180198ltrim xs with (strM xs)
181199 ltrim "" | StrNil = ""
@@ -185,15 +203,17 @@ ltrim xs with (strM xs)
185203||| Removes whitespace (determined with 'isSpace') from
186204||| the start and end of the string.
187205|||
188−||| Idris> trim " A\nB C "
189−||| "A\nB C" : String
206+||| ```idris example
207+||| trim " A\nB C "
208+||| ```
190209trim : String -> String
191210trim xs = ltrim (reverse (ltrim (reverse xs)))
192211
193212||| Splits a character list into a list of whitespace separated character lists.
194213|||
195−||| Idris> words' (unpack " A B C D E ")
196−||| [['A'], ['B'], ['C'], ['D'], ['E']] : List (List Char)
214+||| ```idris example
215+||| words' (unpack " A B C D E ")
216+||| ```
197217words' : List Char -> List (List Char)
198218words' s = case dropWhile isSpace s of
199219 [] => []
@@ -202,15 +222,17 @@ words' s = case dropWhile isSpace s of
202222
203223||| Splits a string into a list of whitespace separated strings.
204224|||
205−||| Idris> words " A B C D E "
206−||| ["A", "B", "C", "D", "E"] : List String
225+||| ```idris example
226+||| words " A B C D E "
227+||| ```
207228words : String -> List String
208229words s = map pack $ words' $ unpack s
209230
210231||| Splits a character list into a list of newline separated character lists.
211232|||
212−||| Idris> lines' (unpack "\rA BC\nD\r\nE\n")
213−||| [['A', ' ', 'B', 'C'], ['D'], ['E']] : List (List Char)
233+||| ```idris example
234+||| lines' (unpack "\rA BC\nD\r\nE\n")
235+||| ```
214236lines' : List Char -> List (List Char)
215237lines' s = case dropWhile isNL s of
216238 [] => []
@@ -219,8 +241,9 @@ lines' s = case dropWhile isNL s of
219241
220242||| Splits a string into a list of newline separated strings.
221243|||
222−||| Idris> lines "\rA BC\nD\r\nE\n"
223−||| ["A BC", "D", "E"] : List String
244+||| ```idris example
245+||| lines "\rA BC\nD\r\nE\n"
246+||| ```
224247lines : String -> List String
225248lines s = map pack $ lines' $ unpack s
226249
@@ -235,8 +258,9 @@ foldl1 f (x::xs) = foldl f x xs
235258
236259||| Joins the character lists by spaces into a single character list.
237260|||
238−||| Idris> unwords' [['A'], ['B', 'C'], ['D'], ['E']]
239−||| ['A', ' ', 'B', 'C', ' ', 'D', ' ', 'E'] : List Char
261+||| ```idris example
262+||| unwords' [['A'], ['B', 'C'], ['D'], ['E']]
263+||| ```
240264unwords' : List (List Char) -> List Char
241265unwords' [] = []
242266unwords' ws = assert_total (foldr1 addSpace ws)
@@ -246,24 +270,28 @@ unwords' ws = assert_total (foldr1 addSpace ws)
246270
247271||| Joins the strings by spaces into a single string.
248272|||
249−||| Idris> unwords ["A", "BC", "D", "E"]
250−||| "A BC D E" : String
273+||| ```idris example
274+||| unwords ["A", "BC", "D", "E"]
275+||| ```
251276unwords : List String -> String
252277unwords = pack . unwords' . map unpack
253278
254279||| Returns the length of the string.
255280|||
256−||| Idris> length ""
257−||| 0 : Nat
258−||| Idris> length "ABC"
259−||| 3 : Nat
281+||| ```idris example
282+||| length ""
283+||| ```
284+||| ```idris example
285+||| length "ABC"
286+||| ```
260287length : String -> Nat
261288length = fromInteger . prim__zextInt_BigInt . prim_lenString
262289
263290||| Lowercases all characters in the string.
264291|||
265−||| Idris> toLower "aBc12!"
266−||| "abc12!" : String
292+||| ```idris example
293+||| toLower "aBc12!"
294+||| ```
267295toLower : String -> String
268296toLower x with (strM x)
269297 strToLower "" | StrNil = ""
@@ -272,14 +300,15 @@ toLower x with (strM x)
272300
273301||| Uppercases all characters in the string.
274302|||
275−||| Idris> toLower "aBc12!"
276−||| "ABC12!" : String
303+||| ```idris example
304+||| toLower "aBc12!"
305+||| ```
277306toUpper : String -> String
278307toUpper x with (strM x)
279308 strToLower "" | StrNil = ""
280309 strToLower (strCons c cs) | (StrCons c cs) =
281310 strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))
282−
311+
283312--------------------------------------------------------------------------------
284313-- Predicates
285314--------------------------------------------------------------------------------