[opentheory-users] WFREC

[Joe Hurd]

Hi Konrad,

> Note that relationTheory is quite simple, in that it is just based on
>
>   'a -> 'a -> bool
>
> That means that there are lots of "wellfoundedness" operators
> that probably shouldn't get transported to relationTheory. I'm thinking
> of "measure" in particular, which has type
>
>   ('a -> num) -> 'a -> 'a -> bool
>
> and belongs in whatever basic theory of natural numbers you've got.

This intertwining of basic theories is just the kind of thing that
OpenTheory was designed to handle. Right now the standard relation
theory

http://opentheory.gilith.com/?pkg=relation

includes subtheories that just depend on basic stuff, and a
relation-natural subtheory that depends on the theory of natural
numbers and defines a 'measure' constant with the type you give.

Cheers,

Joe