af9f826 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Renamed VectFun to FunN, added a few explanatory comments.

af9f826Timo Petteri Sinnemäki13 years ago

libs/base/Data/FunN.idrnew file+8

compare with master

unifiedsplit

@@ -0,0 +1,8 @@

1+module Data.FunN

3+--------------------------------------------------------------------------------

4+-- Build an n-ary function type from a Vect of Types and a result type

5+--------------------------------------------------------------------------------

6+FunN : Vect n Type -> Type -> Type

7+FunN [] r = r

8+FunN (t::ts) r = t -> FunN ts r

libs/base/Data/Rel.idr+6−3

@@ -1,10 +1,13 @@

1module Data.Rel

3−import Data.VectFun

3+import Data.FunN

5+--------------------------------------------------------------------------------

6+-- Build an n-ary relation type from a Vect of Types

7+--------------------------------------------------------------------------------

5Rel : Vect n Type -> Type

8Rel : Vect n Type -> Type

6−Rel ts = VectFun ts Type

9+Rel ts = FunN ts Type

8−liftRel : (ts : Vect k Type) -> (p : Rel ts) -> (Type -> Type) -> Type

11+liftRel : (ts : Vect n Type) -> (p : Rel ts) -> (Type -> Type) -> Type

9liftRel [] p f = f p

12liftRel [] p f = f p

10liftRel (t :: ts) p f = (x : t) -> liftRel ts (p x) f

13liftRel (t :: ts) p f = (x : t) -> liftRel ts (p x) f

libs/base/Data/VectFun.idrdeleted−5

@@ -1,5 +0,0 @@

1−module Data.VectFun

2−

3−VectFun : Vect n Type -> Type -> Type

4−VectFun [] r = r

5−VectFun (t::ts) r = t -> VectFun ts r

libs/base/Decidable/Decidable.idr+2

@@ -8,6 +8,8 @@ import Data.Rel

8-- Typeclass for decidable n-ary Relations

9--------------------------------------------------------------------------------

11+-- Note: Instance resolution for Decidable is likely to not work in the REPL

12+-- at the moment.

11class Decidable (ts : Vect k Type) (p : Rel ts) where

13class Decidable (ts : Vect k Type) (p : Rel ts) where

12 total decide : liftRel ts p Dec

14 total decide : liftRel ts p Dec