Re: [isabelle] monadic function definition



Sorry, I wanted to point at


http://isabelle.in.tum.de/website-Isabelle2014-RC3/dist/library/HOL/HOL-Library/Monad_Syntax.html

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

cheers

chris

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

http://www4.in.tum.de/~krauss/


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

http://isabelle.in.tum.de/nominal/activities/idw10/idw.html

Best,
Andreas

On 11/08/14 15:41, Gergely Buday wrote:
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.