# Re: [isabelle] about longer computation syntax sugar

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'"
nonterminals
dobind
syntax
"_bind" :: "[pttrn, 'a] => dobind" ("(2_ <-/ _)" 10)
"_do" :: "[dobind, 'a] => 'b" ("( do _ ;/ _
od )" [0,0] 10)
translations
" 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.
cheers:)
Liu Jian
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.
>
> Cheers,
> Gerwin
>
--
email to: gjk.liu at gmail.com

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*