blob: 54ac7adada860dd7f9d694ec7514a4c3efdd3b06 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
module DepType
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
-- The finite sets.
|
