Re: [isabelle] recursive functions and set comprehension



Dimitrios,

Hello all, consider the (admittedly strange) fragment:

datatype tm = Z | S "tm"

consts foo :: "tm => tm set"
recdef foo "measure size"
"foo x = { Z. (x = Z) } \<union>
         { (S x1) | x1. x = S x1 /\ x1 : (foo x1) }";


Also note that in the first comprehension, Z is parsed as a bound variable ("The set of all Z, where x equals Z"). Is this really what you want?

Alex





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