git.iko.soy/Idris-dev
on master help sign in
Remove force/lazy
00793acEdwin Brady
libs/prelude/Builtins.idr+1−6
compare with master
unifiedsplit
@@ -38,17 +38,12 @@ sym refl = refl
38trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
38trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
39trans refl refl = refl
39trans refl refl = refl
40
40
41−lazy : a -> a
42−lazy x = x -- compiled specially
43−
44−force : a -> a
45−force x = x -- compiled specially
46−
47||| There are two types of laziness: that arising from lazy functions, and that
41||| There are two types of laziness: that arising from lazy functions, and that
48||| arising from codata. They differ in their totality condition.
42||| arising from codata. They differ in their totality condition.
49data LazyType = LazyCodata | LazyEval
43data LazyType = LazyCodata | LazyEval
50
44
51||| The underlying implementation of Lazy and Inf.
45||| The underlying implementation of Lazy and Inf.
46+%error_reverse
52data Lazy' : LazyType -> Type -> Type where
47data Lazy' : LazyType -> Type -> Type where
53 ||| A delayed computation.
48 ||| A delayed computation.
54 |||
49 |||
libs/prelude/Prelude/List.idr−7
@@ -195,13 +195,6 @@ list nil cons (x::xs) = (Force cons) x xs
195(++) [] right = right
195(++) [] right = right
196(++) (x::xs) right = x :: (xs ++ right)
196(++) (x::xs) right = x :: (xs ++ right)
197
197
198−||| Create an infinite sequence of some item.
199−|||
200−||| Consider using a `Stream` instead.
201−partial
202−repeat : a -> List a
203−repeat x = x :: lazy (repeat x)
204−
205||| Construct a list with `n` copies of `x`
198||| Construct a list with `n` copies of `x`
206||| @ n how many copies
199||| @ n how many copies
207||| @ x the element to replicate
200||| @ x the element to replicate