search

DeepSpec / InteractionTrees

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

Add MonadPropT to master #236

Closed euisuny closed 2 years ago

euisuny commented 2 years ago

Porting over PropT and relevant proofs from vellvm (https://github.com/vellvm/vellvm/blob/dev/src/coq/Utils/PropT.v)

Lysxia commented 2 years ago

The Basics namespace is things that don't depend on itrees. So Basics.MonadPropT should be moved into its own directory. Also since PropT is no longer a transformer, there should be a better name for it. Since it's a set of itrees, can we call it iforest?

euisuny commented 2 years ago

Sure, sounds good to me! That's a nifty name.

Lysxia commented 2 years ago

I wonder if bind could be made lawful using an ad hoc "bind-like" relation, instead of using bind and eutt. But I'm not going to let that block this PR.