on master help sign in
Add a canonical Char→String function and Cast instance
968d433Melvar Chen
lib/Prelude/Strings.idr+6
@@ -42,12 +42,18 @@ unpack s with (strM s)
42pack : (Foldable t) => t Char -> String
42pack : (Foldable t) => t Char -> String
43pack = foldr strCons ""
43pack = foldr strCons ""
44
44
45+singleton : Char -> String
46+singleton c = strCons c ""
47+
45instance Cast String (List Char) where
48instance Cast String (List Char) where
46 cast = unpack
49 cast = unpack
47
50
48instance Cast (List Char) String where
51instance Cast (List Char) String where
49 cast = pack
52 cast = pack
50
53
54+instance Cast Char String where
55+ cast = singleton
56+
51instance Semigroup String where
57instance Semigroup String where
52 (<+>) = (++)
58 (<+>) = (++)
53
59