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