Re: [isabelle] Numeral is acting strangely
0 and 1 are constants in their own right. They are not made by
number_of. Their number_of equivalents are displayed as Numeral0 and
Numeral1. Having 0 and 1 as constants allows them to be involved in
many axiomatic type classes concerning algebraic properties. Users
normally should not notice.
A related issue: for type nat, while 1 = Suc 0, this is not a
On 3 Jul 2006, at 09:55, Rafal Kolanski wrote:
As far as I can understand numerals, both sides should be number_of
Gentlemen, what gives?
This archive was generated by a fusion of
Pipermail (Mailman edition) and