Consolidate stateT to extlib?

[elefthei]

Why is state and stateT defined both in ext-lib and Basics.v https://github.com/coq-community/coq-ext-lib/blob/master/theories/Data/Monads/StateMonad.v https://github.com/DeepSpec/InteractionTrees/blob/master/theories/Basics/Basics.v

[Lysxia]

In hindsight I agree it's worth switching to ext-lib's definition, if only to make things less confusing.

My thought at the time was that ext-lib's stateT was meant to mimick the StateT newtype in Haskell, but in Coq newtypes are not really necessary since they can just as well be Definition, so I was experimenting with doing things this way. In the end I think it's more trouble than it's worth, and a stronger distinction between stateT and its unfolding may actually be quite useful in places.

[elefthei]

I am indifferent to newtype vs definition, maybe I slightly prefer definition because it requires one less constructor to keep track of. But I do have strong preference for no duplication, if that seems reasonable I can fix on the next version (not sure when this will be)

[gmalecha]

The motivation for the constructor was to aid in error messages. When writing monadic computations, having an extra lamba is something that is not very uncommon when changing code and getting a good error message is very useful.

[elefthei]

This makes sense, thanks for the clarification! Will keep ext-lib stateT and import it in InteractionTrees