Renamed VectFun to FunN, added a few explanatory comments.
commitaf9f826f2a34916aa2c137dd89e2321c8b9c0ba1
authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi>
dateMon 20 Jan 2014, 01:50 (13 years ago)
parent1b511c7
libs/base/Data/FunN.idrnew file+8
@@ -0,0 +1,8 @@
1+module Data.FunN
2+
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 @@
11module Data.Rel
22
3−import Data.VectFun
3+import Data.FunN
44
5+--------------------------------------------------------------------------------
6+-- Build an n-ary relation type from a Vect of Types
7+--------------------------------------------------------------------------------
58Rel : Vect n Type -> Type
6−Rel ts = VectFun ts Type
9+Rel ts = FunN ts Type
710
8−liftRel : (ts : Vect k Type) -> (p : Rel ts) -> (Type -> Type) -> Type
11+liftRel : (ts : Vect n Type) -> (p : Rel ts) -> (Type -> Type) -> Type
912liftRel [] p f = f p
1013liftRel (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
88-- Typeclass for decidable n-ary Relations
99--------------------------------------------------------------------------------
1010
11+-- Note: Instance resolution for Decidable is likely to not work in the REPL
12+-- at the moment.
1113class Decidable (ts : Vect k Type) (p : Rel ts) where
1214 total decide : liftRel ts p Dec
1315