Define Prelude.List.replicate in a way that doesn’t require %assert_total
commitd8dd3659ac061079ac4ace36d02caba937f14abf
authorMelvar Chen <Melvar.Chen@googlemail.com>
dateWed 3 Jul 2013, 20:56 (13 years ago)
parentdad12e6
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