diff options
Diffstat (limited to 'src/Inky/Data/List.idr')
| -rw-r--r-- | src/Inky/Data/List.idr | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/src/Inky/Data/List.idr b/src/Inky/Data/List.idr deleted file mode 100644 index 24cb9c0..0000000 --- a/src/Inky/Data/List.idr +++ /dev/null @@ -1,13 +0,0 @@ -module Inky.Data.List - -public export -data LengthOf : List a -> Type where - Z : LengthOf [] - S : LengthOf xs -> LengthOf (x :: xs) - -%name LengthOf len - -public export -lengthOf : (xs : List a) -> LengthOf xs -lengthOf [] = Z -lengthOf (x :: xs) = S (lengthOf xs) |