Merge pull request #3547 from Termina1/patch-1
Change export rules for Data.String.Views module
commit327a423c4d83a5d484f2d0d25807e1448b9a13ab
authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com>
dateMon 5 Dec 2016, 13:20 (10 years ago)
parent01aff977eed681
CONTRIBUTORS+1
@@ -206,6 +206,7 @@ TorosFanny
206206Trevor Elliott
207207uwap
208208Vitaly Bragilevsky
209+Vyacheslav Shebanov
209210xged
210211XIE Yuheng
211212Yacine Hmito
libs/base/Data/String/Views.idr+2
@@ -1,5 +1,7 @@
11module Data.String.Views
22
3+%access public export
4+
35||| View for traversing a String one character at a time
46data StrList : String -> Type where
57 SNil : StrList ""