/coq-itree-io

Interpreter from itree to IO

Primary LanguageCoqMIT LicenseMIT

Run interaction trees in IO

Docker CI

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.