Added Data.String.Views
Currently only has a traversal of strings as characters. More to be
added!
commit59d44d401e7bec015f619f9c05917e3c86aab721
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateFri 29 Apr 2016, 14:55 (10 years ago)
parentd280640
idris.cabal+1
@@ -117,6 +117,7 @@ Extra-source-files:
117117 libs/base/Data/Nat/*.idr
118118 libs/base/Data/List/*.idr
119119 libs/base/Data/Vect/*.idr
120+ libs/base/Data/String/*.idr
120121 libs/base/Debug/*.idr
121122 libs/base/Language/Reflection/*.idr
122123 libs/base/Makefile
libs/base/Data/Nat/Views.idr+1−1
@@ -1,7 +1,7 @@
11module Data.Nat.Views
22
3−public export
43||| View for dividing a Nat in half
4+public export
55data Half : Nat -> Type where
66 HalfOdd : {n : Nat} -> Half (S (n + n))
77 HalfEven : {n : Nat} -> Half (n + n)
libs/base/Data/String/Views.idrnew file+13
@@ -0,0 +1,13 @@
1+module Data.String.Views
2+
3+||| View for traversing a String one character at a time
4+data StrList : String -> Type where
5+ SNil : StrList ""
6+ SCons : (x : Char) -> (rec : StrList xs) -> StrList (strCons x xs)
7+
8+||| Covering function for `StrList`
9+strList : (x : String) -> StrList x
10+strList x with (strM x)
11+ strList "" | StrNil = SNil
12+ strList (strCons y xs) | (StrCons y xs)
13+ = assert_total $ SCons y (strList xs)
libs/base/base.ipkg+1
@@ -19,6 +19,7 @@ modules = System,
1919 Data.Erased, Data.List, Data.List.Views,
2020 Data.List.Quantifiers,
2121 Data.Nat.Views,
22+ Data.String.Views,
2223 Data.So, Data.String,
2324
2425 Control.Isomorphism,