Re: [isabelle] about longer computation syntax sugar
you need to do the rest as well, see lines 125-192 in
HOL/Library/StateMonad.thy. The file is part of Isabelle2008 already, I
believe, if not, you can find it in the Isabelle development snapshot.
Specifically, you will need _scomp (and _fcomp if you want to leave out the
"_ <-" part) and for printing also the ML print translation. Florian Haftmann
wrote that specific theory, he'll be able to explain in more detail how it works.
Liu Jian wrote:
Thanks Gerwin! following your direction, I write the following statements
types ('s, 'a)state_monad = " 's => ('a , 's)"
constdefs bind :: "('s, 'a)state_monad =>('a => ('s, 'b)state_monad)
=>('s, 'b)state_monad" (infixr ">>=" 60)
" f >>= g == % s . let (v, s') = f s in g v s'"
"_bind" :: "[pttrn, 'a] => dobind" ("(2_ <-/ _)" 10)
"_do" :: "[dobind, 'a] => 'b" ("( do _ ;/ _
od )" [0,0] 10)
" do x <- f ; g od" == " f >>= (% x. g)"
Now, binding two monads is easy. But How to bind three or more monads
in a "do ... od"
statement? Moreover, what is the association attribute of "bind"
operator? infixr or infixl.
In the above definition I use the former. But I can not hold the
difference between them.
On Wed, Nov 26, 2008 at 6:49 PM, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:
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