Idris2/tests/idris2/linear003/Linear.idr
Edwin Brady a972778eab Add test script
They don't all pass yet, for minor reasons. Coming shortly...
Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 18:25:18 +01:00

49 lines
970 B
Idris

data Nat : Type where
Z : Nat
S : (1 k : Nat) -> Nat
data Bool : Type where
False : Bool
True : Bool
data Thing : Bool -> Type where
TF : Thing False
TT : Thing True
data Maybe : Type -> Type where
Nothing : {a : Type} -> Maybe a
Just : {a : Type} -> a -> Maybe a
ok : (0 b : Bool) -> Thing b -> Bool
ok False TF = True
ok True TT = False
id : {a : Type} -> (1 x : a) -> a
id x = x
test : (1 x : Nat) -> Nat
test x = id x
data Pair : Type -> Type -> Type where
MkPair : (1 x : a) -> (0 y : b) -> Pair a b
fst : (1 p : Pair a b) -> a
fst (MkPair x y) = x
wibble : (1 p : Pair a b) -> a
wibble {a=a} (MkPair x y)
= let test : (1 y : a) -> a
test y = y in
test x
plus : (1 x : Nat) -> (1 y : Nat) -> Nat
plus Z y = y
plus (S k) y = S (plus k y)
holetest1 : (1 x : Nat) -> (1 y : Nat) -> Nat
holetest1 x y = plus ?this y
holetest2 : (1 x : Nat) -> (1 y : Nat) -> Nat
holetest2 x y = plus x ?that