Re: [isabelle] recursive functions and set comprehension


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?


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