Re: [isabelle] monadic function definition

Sorry, I wanted to point at

in my last email, but forgot it. There you can see the actual translation (keyword "translations"), which tells you everything there is to know about do-notation (using itself the more basic adhoc overloading mechanism).



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

Do-notation has been presented at the Isabelle Developer Workshop in
2010 by Christian Sternagel. His slides are available at:


On 11/08/14 15:41, Gergely Buday wrote:

I have found

partial_function (option)
   collatz :: "nat ⇒ nat list option"
   "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:

- Gergely

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