*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] monadic function definition*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Mon, 11 Aug 2014 16:22:14 +0200*In-reply-to*: <53E8C9E9.3000709@inf.ethz.ch>*References*: <CA+3iOznxk7GvnBSwfXEucDnWJ+RB+jzxO8q3d9B4Ejb=54b2WQ@mail.gmail.com> <53E8C9E9.3000709@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.7.0

Hi Gergely,

cheers chris On 08/11/2014 03:49 PM, Andreas Lochbihler wrote:

Hi Gergely, Definitions of recursive functions in a monad with execptions (via partial_function) is described in Alex Krauss' paper at PAR 2010 available from http://www4.in.tum.de/~krauss/ Do-notation has been presented at the Isabelle Developer Workshop in 2010 by Christian Sternagel. His slides are available at: http://isabelle.in.tum.de/nominal/activities/idw10/idw.html Best, Andreas On 11/08/14 15:41, Gergely Buday wrote:Hi, I have found partial_function (option) collatz :: "nat ⇒ nat list option" where "collatz n = (if n ≤ 1 then Some [n] else if even n then do { ns ← collatz (n div 2); Some (n # ns) } else do { ns ← collatz (3 * n + 1); Some (n # ns)})" in src/HOL/Ex/Fundefs.thy Where can I find a description of such monadic definitions? I did not find it in the Isar reference and what I have found was the early history of it: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-May/msg00055.html - Gergely

**Follow-Ups**:**Re: [isabelle] monadic function definition***From:*Gergely Buday

**References**:**[isabelle] monadic function definition***From:*Gergely Buday

**Re: [isabelle] monadic function definition***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] monadic function definition
- Next by Date: Re: [isabelle] monadic function definition
- Previous by Thread: Re: [isabelle] monadic function definition
- Next by Thread: Re: [isabelle] monadic function definition
- Cl-isabelle-users August 2014 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