This first example gives a clear demonstration of the nature of the
syntactic translation that the monad syntax implements because there
is no specific enabled monad for the syntax to map to:
> monadsyntax.enable_monadsyntax();
val it = () : unit
> “do M1 ; M2; od”;
val it = “monad_unitbind M1 M2” : term;
> “do v <- M1; w <- M2 v 3; return (v + w); od”;
val it = “monad_bind M1 (λv. monad_bind (M2 v 3) (λw. return (v + w)))”
: term
The monad_bind, monad_unitbind and return terms above are
variables that would be instantiated with the appropriate terms
given the available choices of enabled monads.