Isabelle wrote:
> I have defined as follows the state-transformer monad type :
>
> :: STM s x = { stm :: s -> ( s , x ) }
...
> I do not send detailed sources here because I suspect there is a basic
> flaw in the STM type definition, clashing with uniqueness typing, but I
> can't see where...
Try
:: STM *s x = { stm :: .(s -> ( s , x )) }
cheers
Martin Wierich