0 | ||| Utilities functions for conditionally delaying values. 1 | module Control.Delayed 2 | 3 | ||| Type-level function for a conditionally infinite type. 4 | public export 5 | inf : Bool -> Type -> Type 6 | inf False t = t 7 | inf True t = Inf t 8 | 9 | ||| Type-level function for a conditionally lazy type. 10 | public export 11 | lazy : Bool -> Type -> Type 12 | lazy False t = t 13 | lazy True t = Lazy t 14 |