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 MHonArc.