@@ -47,7 +47,7 @@ data LazyType = LazyCodata | LazyEval
47data Lazy' : LazyType -> Type -> Type where
47data Lazy' : LazyType -> Type -> Type where
48 ||| A delayed computation.
48 ||| A delayed computation.
50− |||Delay is inserted automatically by the elaborator where necessary.
50+ ||| Delay is inserted automatically by the elaborator where necessary.
52 ||| Note that compiled code gives `Delay` special semantics.
52 ||| Note that compiled code gives `Delay` special semantics.
53 ||| @ t whether this is laziness from codata or normal lazy evaluation
53 ||| @ t whether this is laziness from codata or normal lazy evaluation