git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/libs/contrib/Data/String.idr
31 lines 512 B history raw
1module Data.String
3infixl 5 +>
4infixr 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||| ```
14strSnoc : String -> Char -> String
15strSnoc s c = s ++ (singleton c)
17||| Alias of `strSnoc`
18|||
19||| ```idris example
20||| "AB" +> 'C'
21||| ```
22(+>) : String -> Char -> String
23(+>) = strSnoc
25||| Alias of `strCons`
26|||
27||| ```idris example
28||| 'A' <+ "AB"
29||| ```
30(<+) : Char -> String -> String
31(<+) = strCons