git.iko.soy/Idris-dev
on master help sign in
Re-rename FunN all the way back to Fun.
commit0c9e3a3fba114ab91c3d6d0818eacb2626b115f3 authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateMon 20 Jan 2014, 11:09 (13 years ago) parent9e1f8fa
3 files changed+7−7
compare with master
unifiedsplit
libs/base/Data/FunN.idr → libs/base/Data/Fun.idr+4−4 libs/base/Data/Rel.idr+2−2 libs/base/base.ipkg+1−1
libs/base/Data/FunN.idr → libs/base/Data/Fun.idrrenamed+4−4
@@ -1,8 +1,8 @@
1−module Data.FunN
1+module Data.Fun
22
33--------------------------------------------------------------------------------
44-- Build an n-ary function type from a Vect of Types and a result type
55--------------------------------------------------------------------------------
6−FunN : Vect n Type -> Type -> Type
7−FunN [] r = r
8−FunN (t::ts) r = t -> FunN ts r
6+Fun : Vect n Type -> Type -> Type
7+Fun [] r = r
8+Fun (t::ts) r = t -> Fun ts r
libs/base/Data/Rel.idr+2−2
@@ -1,12 +1,12 @@
11module Data.Rel
22
3−import Data.FunN
3+import Data.Fun
44
55--------------------------------------------------------------------------------
66-- Build an n-ary relation type from a Vect of Types
77--------------------------------------------------------------------------------
88Rel : Vect n Type -> Type
9−Rel ts = FunN ts Type
9+Rel ts = Fun ts Type
1010
1111liftRel : (ts : Vect n Type) -> (p : Rel ts) -> (Type -> Type) -> Type
1212liftRel [] p f = f p
libs/base/base.ipkg+1−1
@@ -23,7 +23,7 @@ modules = System,
2323 Data.ZZ, Data.Sign,
2424 Data.SortedMap, Data.SortedSet, Data.BoundedList,
2525 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
26− Data.Floats, Data.Complex, Data.Heap, Data.FunN,
26+ Data.Floats, Data.Complex, Data.Heap, Data.Fun,
2727 Data.Rel,
2828
2929 Control.Isomorphism,