-
Notifications
You must be signed in to change notification settings - Fork 1
IO using sized types and copatterns
License
gallais/agda-sizedIO
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
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
About
IO using sized types and copatterns
Topics
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published