The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 13/03/2016 19:56, Lars Rasmusson wrote:
> (Probably I have made an error somewhere, but I'm not able to spot it.)

Your monad is a CPS, which typically requires impredicativity of the
target sort to be run into the same sort. I think this is why your
example fails. If this is the case, there is not much to do to be able
to port this code to Coq, except maybe using the -impredicative-set flag.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature