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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and