Re: [isabelle] monadic function definition

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.