separate crun out of MonadTypedStore

affeldt-aist / monae

Monadic effects and equational reasonig in Coq

GNU Lesser General Public License v2.1

68 stars 12 forks source link

Closed t6s closed 4 months ago

t6s commented 4 months ago

This PR splits MonadTypedStore in the hierarchy into MonadTypedStore and MonadTypedStoreRun.

garrigue commented 4 months ago

By the way, I also see some [the ...] left around. I should fix it eventually.

t6s commented 4 months ago

@garrigue I have made changes according to your suggestions. Almost everything was straightforward, but one proof needed a small change.

garrigue commented 4 months ago

@t6s LGTM Thanks