Make 'repeat' run lazily
Needs 'lazy' in the recursive call otherwise it will run forever when
compiled.
Fixes issue #352
commiteb08982b81e5df8c6f81ee22911fa78094d7097f
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateTue 25 Jun 2013, 22:13 (13 years ago)
parent1b589f8
lib/Prelude/List.idr+1−1
@@ -123,7 +123,7 @@ length (x::xs) = 1 + length xs
123123
124124partial
125125repeat : a -> List a
126−repeat x = x :: repeat x
126+repeat x = x :: lazy (repeat x)
127127
128128%assert_total
129129replicate : Nat -> a -> List a