Re: [isabelle] about longer computation syntax sugar
Liu Jian wrote:
do x <- f; g x od == f >>= g
But how to write the real isabelle statements for the above
definition? (Note there is parameter "x")
It's fairly standard syntax black magic and works roughly like the normal let
bindings in Isabelle (e.g. see HOL/HOL.thy).
A more complex example directly with "do" syntax can be found in
HOL/Library/StateMonad.thy. It's slightly different from the one in our
papers, but the effect is the same.
This archive was generated by a fusion of
Pipermail (Mailman edition) and