@@ -38,17 +38,12 @@ sym refl = refl
3838trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
3939trans refl refl = refl
4040
41−lazy : a -> a
42−lazy x = x -- compiled specially
43−
44−force : a -> a
45−force x = x -- compiled specially
46−
4741||| There are two types of laziness: that arising from lazy functions, and that
4842||| arising from codata. They differ in their totality condition.
4943data LazyType = LazyCodata | LazyEval
5044
5145||| The underlying implementation of Lazy and Inf.
46+%error_reverse
5247data Lazy' : LazyType -> Type -> Type where
5348 ||| A delayed computation.
5449 |||