[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.