Skip to content

liyishuai/coq-itree-io

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

10 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Run interaction trees in IO

CircleCI

Interpret itree in the IO monad of simple-io.

Overview

From ITreeIO Require Import ITreeIO.

(* Provides the following function (and a few other variants) *)
Parameter interp_io : forall E : Type -> Type, (E ~> IO) -> (itree E ~> IO).
Arguments interp_io {E} h [T] t.

About

Interpreter from itree to IO

Resources

License

Code of conduct

Stars

Watchers

Forks

Releases

No releases published

Sponsor this project

 

Packages

No packages published

Languages

  • Coq 78.1%
  • Makefile 21.9%