src/Inky/Data/List.idr


1
2
3
4
5
6
7
8
9
10
11
12
13

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)