git.iko.soy/Idris-dev
on master help sign in
Define Prelude.List.replicate in a way that doesn’t require %assert_total
d8dd365Melvar Chen
lib/Prelude/List.idr+2−2
compare with master
unifiedsplit
@@ -125,9 +125,9 @@ partial
125repeat : a -> List a
125repeat : a -> List a
126repeat x = x :: lazy (repeat x)
126repeat x = x :: lazy (repeat x)
127
127
128−%assert_total
129replicate : Nat -> a -> List a
128replicate : 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
131
131
132--------------------------------------------------------------------------------
132--------------------------------------------------------------------------------
133-- Instances
133-- Instances