git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/base/Data/Rel.idr
12 lines 283 B history raw
1module Data.Rel
3import Data.Fun
6||| Build an n-ary relation type from a Vect of Types
7Rel : Vect n Type -> Type
8Rel ts = Fun ts Type
10liftRel : (ts : Vect n Type) -> (p : Rel ts) -> (Type -> Type) -> Type
11liftRel [] p f = f p
12liftRel (t :: ts) p f = (x : t) -> liftRel ts (p x) f