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 syntactic identity.

Larry Paulson


On 3 Jul 2006, at 09:55, Rafal Kolanski wrote:

As far as I can understand numerals, both sides should be number_of (Pls).

Gentlemen, what gives?






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.