[opentheory-users] numerals

[Ramana Kumar]

The OpenTheory inference system shows a clear bias in favour of HOL Light.
This is manifest in the amount of extra work developers of other systems would
need to do to write article readers and writers compared to of HOL Light. But
I think that is OK because the HOL Light inference system is clean and
minimal-looking.

However, the bias evident in the standard library numerals is not so great.
Norrish numerals (bit1 and bit2) are "clearly superior" to binary (bit0 and
bit1) because the representations are unique. There are other options too, such
as lists of decimal digits. Possibly the standard library doesn't need numerals
at all (i.e. use unary numerals with suc and zero), if we don't anticipate very
large natural number constants actually appearing in theorems.

My main purpose in writing is to start a discussion, because I'm not
particularly aware of the issues and trade-offs regarding numerals but I see
there might be a possibility for improved design. I also don't know the extent
of the effects of making the right choice for the standard library. Maybe it is
too small to be worth the effort?