||| Utilities functions for contitionally delaying values.module Control.Delayed %default total ||| Type-level function for a conditionally delayed type (`Lazy` or `Inf`).public exportdelayed : DelayReason -> Bool -> Type -> Typedelayed r False a = adelayed r True a = Delayed r a ||| Type-level function for a conditionally infinite type.public exportinf : Bool -> Type -> Typeinf = delayed Infinite ||| Type-level function for a conditionally lazy type.public exportlazy : Bool -> Type -> Typelazy = delayed LazyValue ||| Conditionally delay a value.exportdelay : {r : DelayReason} -> (d : Bool) -> a -> delayed r d adelay False x = xdelay {r=Infinite}  True x = Delay xdelay {r=LazyValue} True x = Delay x