blob: f85a595addbd4ec806d169353d41b3c3c0d7f45d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
module DepType
import Data.Fin
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False (x :: xs) = x + sum False xs
data MyVect : Nat -> Type -> Type where
Nil : MyVect Z a
(::) : a -> MyVect k a -> MyVect (S k) a
(++) : MyVect k a -> MyVect l a -> MyVect (k + l) a
(++) [] ys = ys
(++) (x :: xs) ys = x :: xs ++ ys
length : MyVect n a -> Nat
length xs {n} = n
|
