packages feed

idris-0.9.13: test/reg039/reg039.idr

module LazyExec

-- The regression that this tests for is broken laziness in the executor.

covering
countdown : Int -> Lazy (List Int)
countdown n = if n > 0
                 then (n :: countdown (n-1))
                 else []

go : IO ()
go = putStrLn $ show (Force (countdown 3))