69 lines
1.3 KiB
Agda
69 lines
1.3 KiB
Agda
module TestCase2
|
|
|
|
data Nat : U where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
plus : Nat -> Nat -> Nat
|
|
plus Z m = m
|
|
-- if this is a capital K on LHS, it fails with a poor error message
|
|
plus (S k) m = S (plus k m)
|
|
|
|
-- -- Example from Jesper talk (translated to case tree)
|
|
max : Nat -> Nat -> Nat
|
|
max Z m = m
|
|
max n Z = n
|
|
max (S k) (S l) = S (max k l)
|
|
|
|
data List : U -> U where
|
|
LN : {a : U} -> List a
|
|
LCons : {a : U} -> a -> List a -> List a
|
|
|
|
data Vect : Nat -> U -> U where
|
|
Nil : {a : U} -> Vect Z a
|
|
Cons : {a : U} {n : Nat} -> a -> Vect n a -> Vect (S n) a
|
|
|
|
-- NEXT Need to handle implicits
|
|
-- I've hacked implicits, but need to figure out indices..
|
|
length : {a : U} {n : Nat} -> Vect n a -> Nat
|
|
length Nil = Z
|
|
length (Cons x xs) = S (length xs)
|
|
|
|
data Unit : U where
|
|
MkUnit : Unit
|
|
|
|
-- This should fail (and does!)
|
|
-- bar : Vect (S Z) Unit
|
|
-- bar = (Cons MkUnit (Cons MkUnit Nil))
|
|
|
|
data Bool : U where
|
|
True : Bool
|
|
False : Bool
|
|
|
|
not : Bool -> Bool
|
|
not True = False
|
|
not False = True
|
|
|
|
|
|
not2 : Bool -> Bool
|
|
not2 True = False
|
|
not2 x = True
|
|
|
|
-- TEST CASE - remove second clause here and expect error
|
|
and : Bool -> Bool -> Bool
|
|
and True y = y
|
|
and False _ = False
|
|
|
|
nand : Bool -> Bool -> Bool
|
|
nand x y = not (case x of
|
|
True => y
|
|
False => False)
|
|
|
|
|
|
-- for stuff like this, we should add Agda () and check for no constructors
|
|
data Void : U where
|
|
|
|
SnocList : U -> U
|
|
SnocList a = List a
|
|
|