[opentheory-users] WFREC

[Ramana Kumar]

I'm thinking about the appropriate namespace for a recursion operator for
wellfounded relations.
In HOL4 it is called WFREC and is in relationTheory.
In fact there is a small suite of related definitions there: RESTRICT,
approx, and the_fun.
I'm wondering if the list has any ideas about an appropriate way to package
these things up (i.e. under what name, or with what other stuff).
I realize I may need to give more background about what they actually do...
(don't have that on me at the moment!)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120125/0cf08f9f/attachment.htm>