git.iko.soy/Idris-dev
on master help sign in
Append Char to String
392123bcchantep
libs/contrib/Data/String.idrnew file+31
compare with master
unifiedsplit
@@ -0,0 +1,31 @@
1+module Data.String
2+
3+infixl 5 +>
4+infixr 5 <+
5+
6+||| Adds a character to the end of the specified string.
7+|||
8+||| ```idris example
9+||| strSnoc "AB" 'C'
10+||| ```
11+||| ```idris example
12+||| strSnoc "" 'A'
13+||| ```
14+strSnoc : String -> Char -> String
15+strSnoc s c = s ++ (singleton 'c')
16+
17+||| Alias of `strSnoc`
18+|||
19+||| ```idris example
20+||| "AB" +> 'C'
21+||| ```
22+(+>) : String -> Char -> String
23+(+>) = strSnoc
24+
25+||| Alias of `strCons`
26+|||
27+||| ```idris example
28+||| 'A' <+ "AB"
29+||| ```
30+(<+) : Char -> String -> String
31+(<+) = strCons