Merge pull request #372 from Melvar/master
Give replicate a simple total definition
commitab215d01a4c744e60991752466295b790ad10451
authorEdwin Brady <edwin.brady@gmail.com>
dateThu 4 Jul 2013, 10:40 (13 years ago)
parentdad12e6d8dd365
lib/Prelude/List.idr+2−2
@@ -125,9 +125,9 @@ partial
125125repeat : a -> List a
126126repeat x = x :: lazy (repeat x)
127127
128−%assert_total
129128replicate : Nat -> a -> List a
130−replicate n x = take n (repeat x)
129+replicate O x = []
130+replicate (S n) x = x :: replicate n x
131131
132132--------------------------------------------------------------------------------
133133-- Instances