agda-sizedIO

agda-sizedIO copied to clipboard

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