git.iko.soy/Idris-dev
on 4e69658 help sign in
Idris-dev/libs/base/Data/String/Views.idr
13 lines 432 B history raw
1module Data.String.Views
3||| View for traversing a String one character at a time
4data StrList : String -> Type where
5 SNil : StrList ""
6 SCons : (x : Char) -> (rec : StrList xs) -> StrList (strCons x xs)
8||| Covering function for `StrList`
9strList : (x : String) -> StrList x
10strList x with (strM x)
11 strList "" | StrNil = SNil
12 strList (strCons y xs) | (StrCons y xs)
13 = assert_total $ SCons y (strList xs)