# [isabelle] monadic function definition

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

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