search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
199 stars 50 forks source link

WIP: compiler with "MTL-style" semantics #142

Closed Lysxia closed 2 years ago

Lysxia commented 4 years ago

The semantics now have type

denote_imp : forall m `{Monad m} ..., imp -> m unit
denote_asm : forall m `{Monad m} ..., asm -> m unit