git.iko.soy/Idris-dev
on b56ef01 help sign in
Idris-dev/test/basic014/basic014.idr
44 lines 810 B history raw
1-- Test pattern unification
3import Data.Vect
5comp : {A : Type} -> {B : (a : A) -> Type} ->
6 {C : (a : A) -> (b : B a) -> Type} ->
7 (f : {a : A} -> (b : B a) -> C a b) ->
8 (g : (a : A) -> B a) ->
9 (a : A) -> C a (g a)
10comp f g a = f (g a)
12add2 : Nat -> Nat
13add2 = comp S S
15data Foo = MkFoo
16data Bar = MkBar
18foo : Foo -> Bar
20bar : Bar -> Nat
22baz : Foo -> Nat
23baz = (comp bar foo)
25comp0 : (B : Nat -> Type) -> ((n : Nat) -> B n) -> Int
26comp0 _ _ = 0
28test00 : Int
29test00 = comp0 _ S
31comp2 : (B : Nat -> Type) ->
32 ((n : Nat) -> (y : B n) -> Int) -> Int
33comp2 _ _ = 0
35test20 : Int
36test20 = comp2 _ dummy
37 where
38 dummy : (n : Nat) -> Vect n Int -> Int
39 dummy _ _ = 0
41test03 : Int
42test03 = comp0 _ dummy where
43 dummy : (n : Nat) -> Int -> Int
44 dummy _ = \x => x