git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3547 from Termina1/patch-1
327a423Jan de Muijnck-Hughes
CONTRIBUTORS+1
compare with master
unifiedsplit
@@ -206,6 +206,7 @@ TorosFanny
206Trevor Elliott
206Trevor Elliott
207uwap
207uwap
208Vitaly Bragilevsky
208Vitaly Bragilevsky
209+Vyacheslav Shebanov
209xged
210xged
210XIE Yuheng
211XIE Yuheng
211Yacine Hmito
212Yacine Hmito
libs/base/Data/String/Views.idr+2
@@ -1,5 +1,7 @@
1module Data.String.Views
1module Data.String.Views
2
2
3+%access public export
4+
3||| View for traversing a String one character at a time
5||| View for traversing a String one character at a time
4data StrList : String -> Type where
6data StrList : String -> Type where
5 SNil : StrList ""
7 SNil : StrList ""