59d44d4 · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

@@ -117,6 +117,7 @@ Extra-source-files:

117 libs/base/Data/Nat/*.idr

118 libs/base/Data/List/*.idr

119 libs/base/Data/Vect/*.idr

120+ libs/base/Data/String/*.idr

120 libs/base/Debug/*.idr

121 libs/base/Debug/*.idr

121 libs/base/Language/Reflection/*.idr

122 libs/base/Language/Reflection/*.idr

122 libs/base/Makefile

123 libs/base/Makefile

libs/base/Data/Nat/Views.idr+1−1

@@ -1,7 +1,7 @@

1module Data.Nat.Views

2

3−public export

4||| View for dividing a Nat in half

3||| View for dividing a Nat in half

4+public export

5data Half : Nat -> Type where

6 HalfOdd : {n : Nat} -> Half (S (n + n))

7 HalfEven : {n : Nat} -> Half (n + n)

libs/base/Data/String/Views.idrnew file+13

@@ -0,0 +1,13 @@

1+module Data.String.Views

2+

3+||| View for traversing a String one character at a time

4+data StrList : String -> Type where

5+ SNil : StrList ""

6+ SCons : (x : Char) -> (rec : StrList xs) -> StrList (strCons x xs)

7+

8+||| Covering function for `StrList`

9+strList : (x : String) -> StrList x

10+strList x with (strM x)

11+ strList "" | StrNil = SNil

12+ strList (strCons y xs) | (StrCons y xs)

13+ = assert_total $ SCons y (strList xs)

libs/base/base.ipkg+1

@@ -19,6 +19,7 @@ modules = System,

19 Data.Erased, Data.List, Data.List.Views,

20 Data.List.Quantifiers,

21 Data.Nat.Views,

22+ Data.String.Views,

22 Data.So, Data.String,

23 Data.So, Data.String,

23

24

24 Control.Isomorphism,

25 Control.Isomorphism,