git.iko.soy/Idris-dev
on master help sign in
change export rules for module
617f8a8Vyacheslav Shebanov
libs/base/Data/String/Views.idr+2
compare with master
unifiedsplit
@@ -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 ""