module README where -- # agda-sizedIO -- Experimental IO using sized types and copatterns -- This library currently relies on: -- * Agda with support for the NO_UNIVERSE_CHECK pragam, and -- a strictly positive IO builtin. -- i.e. post commit eabd7f5d27f7cf91ee4d70d64ea187a0fd99dab0 -- * Agda's stdlib with: -- - the new codata modules -- - the new Foreign.Haskell.Coerce module -- * The following Haskell packages: -- - directory >= 1.3.2.0 -- - filepath >= 1.4.2.1 -- Examples import cat import read import stopwatch import find import lsR -- Main module import Codata.IO -- Example of bindings import System.Clock.Primitive import System.Clock import System.CPUTime.Primitive import System.CPUTime import System.Environment.Primitive import System.Environment import System.FilePath.Posix.Primitive import System.FilePath.Posix import System.Directory.Primitive import System.Directory import System.Info -- Example of a high-level library function built on top import System.Directory.Tree