diff options
| author | Kjetil Orbekk <kjetil.orbekk@gmail.com> | 2017-02-13 19:09:52 -0500 |
|---|---|---|
| committer | Kjetil Orbekk <kjetil.orbekk@gmail.com> | 2017-02-13 19:09:52 -0500 |
| commit | 202ef8c368d08a3af27655e71772febdd7554351 (patch) | |
| tree | 573b8e57dc0d44c72734f26dbcbbc52fe8fc0955 /DepType.idr | |
| parent | 11082ee77ac7e980680d5ca45df9a84ad55641d2 (diff) | |
Exercises from Idris book.
Chapters 8 and 9.
Diffstat (limited to 'DepType.idr')
| -rw-r--r-- | DepType.idr | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/DepType.idr b/DepType.idr index 54ac7ad..f85a595 100644 --- a/DepType.idr +++ b/DepType.idr @@ -1,4 +1,6 @@ module DepType + +import Data.Fin isSingleton : Bool -> Type isSingleton True = Nat @@ -16,4 +18,5 @@ data MyVect : Nat -> Type -> Type where (++) [] ys = ys (++) (x :: xs) ys = x :: xs ++ ys --- The finite sets. +length : MyVect n a -> Nat +length xs {n} = n |