package coq-simple-io
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
IO monad for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
1.10.0.tar.gz
sha512=004bc44e42d03f9d936fb512191a4e547a228a7db233b1b7aa244f4d8c2d893f2fc9f263008ad72a38b82465dd56f78d92005e0aca626a99d30ad08ec7e7afd8
Description
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 Stdlib module are provided. Users are free to define their own APIs on top of this IO type.
On This Page