*To*: Liu Jian <gjk.liu at gmail.com>*Subject*: Re: [isabelle] about longer computation syntax sugar*From*: Gerwin Klein <gerwin.klein at nicta.com.au>*Date*: Fri, 28 Nov 2008 22:07:33 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <8c2dc7030811270724l6731ddbfr4e2e4d67d8acfa53@mail.gmail.com>*References*: <8c2dc7030811252119x2e9adc04j711b378d57aeaebe@mail.gmail.com> <492D29BF.2090900@nicta.com.au> <8c2dc7030811270724l6731ddbfr4e2e4d67d8acfa53@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.18 (Macintosh/20081105)

Hi Liu,

Specifically, you will need _scomp (and _fcomp if you want to leave out the

Cheers, Gerwin 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'" 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

**Follow-Ups**:**Re: [isabelle] about longer computation syntax sugar***From:*Liu Jian

**References**:**[isabelle] about longer computation syntax sugar***From:*Liu Jian

**Re: [isabelle] about longer computation syntax sugar***From:*Gerwin Klein

**Re: [isabelle] about longer computation syntax sugar***From:*Liu Jian

- Previous by Date: [isabelle] load HOL4
- Next by Date: [isabelle] ACKERMANN AWARD 2009: CALL FOR NOMINATIONS
- Previous by Thread: Re: [isabelle] about longer computation syntax sugar
- Next by Thread: Re: [isabelle] about longer computation syntax sugar
- Cl-isabelle-users November 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list