git.iko.soy/Idris-dev
on master help sign in
Merge pull request #31 from MekeorMelire/master

Added new functions in standard-library

commitfe4997ecede314b2c8674388e2a228e1715635bb authorEdwin Brady <edwin.brady@gmail.com> dateMon 11 Jun 2012, 03:18 (14 years ago) parent906fe5cf67b721
3 files changed+20−2
compare with master
unifiedsplit
lib/prelude/list.idr+7−1 lib/prelude/nat.idr+8 lib/prelude/vect.idr+5−1
lib/prelude/list.idr+7−1
@@ -109,13 +109,19 @@ length [] = 0
109109length (x::xs) = 1 + length xs
110110
111111--------------------------------------------------------------------------------
112−-- Building bigger lists
112+-- Building (bigger) lists
113113--------------------------------------------------------------------------------
114114
115115(++) : List a -> List a -> List a
116116(++) [] right = right
117117(++) (x::xs) right = x :: (xs ++ right)
118118
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+
119125--------------------------------------------------------------------------------
120126-- Instances
121127--------------------------------------------------------------------------------
lib/prelude/nat.idr+8
@@ -44,6 +44,14 @@ total power : Nat -> Nat -> Nat
4444power base O = S O
4545power base (S exp) = mult base $ power base exp
4646
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+
4755--------------------------------------------------------------------------------
4856-- Comparisons
4957--------------------------------------------------------------------------------
lib/prelude/vect.idr+5−1
@@ -64,7 +64,7 @@ fromList [] = []
6464fromList (x::xs) = x :: fromList xs
6565
6666--------------------------------------------------------------------------------
67−-- Building bigger vectors
67+-- Building (bigger) vectors
6868--------------------------------------------------------------------------------
6969
7070total
@@ -72,6 +72,10 @@ total
7272(++) [] ys = ys
7373(++) (x::xs) ys = x :: xs ++ ys
7474
75+replicate : (n : Nat) -> a -> Vect a n
76+replicate O x = []
77+replicate (S k) x = x :: replicate k x
78+
7579--------------------------------------------------------------------------------
7680-- Maps
7781--------------------------------------------------------------------------------