Re: [isabelle] sets in HOL/CF



Brian Huffman wrote:
If you want to be able to define a function of type "nat -> nat set"
with fixrec, it turns out that fixrec can do it, but it requires you
to do some work to set things up first.

A related remark: A recursive function that returns a set can also be defined using the inductive(_set) package. You have to rephrase the definition using introduction rules, and manually derive the recursive equations afterwards, but that is usually straightforward.

Alex





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