coq-simple-io

IO monad for Coq This library provides tools to implement IO programs directly in Coq, in a similar style to Haskell. Facilities for formal verification are not included. IO is defined as a parameter with a purely functional interface in Coq, to be extracted to OCaml. Some wrappers for the basic types and functions in the OCaml Pervasives module are provided. Users are free to define their own APIs on top of this IO type.

opam install coq-simple-io.0.2
homepage
https://github.com/Lysxia/coq-simple-io
license
MIT
bugs tracker
https://github.com/Lysxia/coq-simple-io/issues
dependencies
coq
source
https://github.com/Lysxia/coq-simple-io/archive/0.2.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-simple-io/coq-simple-io.0.2