Split out new module StdEffects from OpenSums (#34)
Rename ITree.ITree to ITree.Core (core definitions), freeing up ITree.ITree for the standard way to open the library.
Operations defined in Core are further wrapped in an ITree module, the intent is that they should be used qualified. (I've had problems caused by shadowing bind and map.)
itree is still at the root of Core so it doesn't need to be qualified, but its actual name is now ITree.Core.itree; we could add notations inside the inner ITree module to "rename" it.
Add embed, yet one more variant of lift, etc., but probably the easiest one to use when defining new effects (see examples/IO.v for example).
StdEffects
fromOpenSums
(#34)ITree.ITree
toITree.Core
(core definitions), freeing upITree.ITree
for the standard way to open the library.Core
are further wrapped in anITree
module, the intent is that they should be used qualified. (I've had problems caused by shadowingbind
andmap
.)itree
is still at the root ofCore
so it doesn't need to be qualified, but its actual name is nowITree.Core.itree
; we could add notations inside the innerITree
module to "rename" it.embed
, yet one more variant oflift
, etc., but probably the easiest one to use when defining new effects (seeexamples/IO.v
for example).