[isabelle] monadic function definition


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.