git.iko.soy/Idris-dev
on master help sign in
Merge pull request #31 from MekeorMelire/master
fe4997eEdwin Brady
lib/prelude/list.idr+7−1
compare with master
unifiedsplit
@@ -109,13 +109,19 @@ length [] = 0
109length (x::xs) = 1 + length xs
109length (x::xs) = 1 + length xs
110
110
111--------------------------------------------------------------------------------
111--------------------------------------------------------------------------------
112−-- Building bigger lists
112+-- Building (bigger) lists
113--------------------------------------------------------------------------------
113--------------------------------------------------------------------------------
114
114
115(++) : List a -> List a -> List a
115(++) : List a -> List a -> List a
116(++) [] right = right
116(++) [] right = right
117(++) (x::xs) right = x :: (xs ++ right)
117(++) (x::xs) right = x :: (xs ++ right)
118
118
119+repeat : a -> List a
120+repeat x = x :: repeat x
121+
122+replicate : Nat -> a -> List a
123+replicate n x = take n (repeat x)
124+
119--------------------------------------------------------------------------------
125--------------------------------------------------------------------------------
120-- Instances
126-- Instances
121--------------------------------------------------------------------------------
127--------------------------------------------------------------------------------
lib/prelude/nat.idr+8
@@ -44,6 +44,14 @@ total power : Nat -> Nat -> Nat
44power base O = S O
44power base O = S O
45power base (S exp) = mult base $ power base exp
45power base (S exp) = mult base $ power base exp
46
46
47+hyper : Nat -> Nat -> Nat -> Nat
48+hyper O a b = S b
49+hyper (S O) a O = a
50+hyper (S(S O)) a O = O
51+hyper n a O = S O
52+hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
53+
54+
47--------------------------------------------------------------------------------
55--------------------------------------------------------------------------------
48-- Comparisons
56-- Comparisons
49--------------------------------------------------------------------------------
57--------------------------------------------------------------------------------
lib/prelude/vect.idr+5−1
@@ -64,7 +64,7 @@ fromList [] = []
64fromList (x::xs) = x :: fromList xs
64fromList (x::xs) = x :: fromList xs
65
65
66--------------------------------------------------------------------------------
66--------------------------------------------------------------------------------
67−-- Building bigger vectors
67+-- Building (bigger) vectors
68--------------------------------------------------------------------------------
68--------------------------------------------------------------------------------
69
69
70total
70total
@@ -72,6 +72,10 @@ total
72(++) [] ys = ys
72(++) [] ys = ys
73(++) (x::xs) ys = x :: xs ++ ys
73(++) (x::xs) ys = x :: xs ++ ys
74
74
75+replicate : (n : Nat) -> a -> Vect a n
76+replicate O x = []
77+replicate (S k) x = x :: replicate k x
78+
75--------------------------------------------------------------------------------
79--------------------------------------------------------------------------------
76-- Maps
80-- Maps
77--------------------------------------------------------------------------------
81--------------------------------------------------------------------------------