Re: [isabelle] monadic function definition



Dear Gergely,

there also is the AFP-entry Partial-Function-MR which allows you to define
sets of mutual recursive partial functions (which is not possible using the 
original partial-function command). In the entry you also find further 
examples of partial functions, including Collatz and a potentially 
non-terminating evaluator for (a kind of) mu-recursive expressions.

Best,
René



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