Obviously, the naturals assign a non-standard meaning to negative numerals.
But are there any types that assign a non-standard meaning to *positive* numerals? (By "standard" I mean 2=1+1, 3=1+1+1, 4=1+1+1+1, etc.) Is there any reason why anyone would ever want to define or use such a type? If not - and if at some point in the future we switch over to unsigned numerals - then I think it might be useful to do to class "number" what we did with class "power" a while back: Replace the overloaded constant with a single, standard definition. In any case, I think such a major change would require a bit of planning, and probably won't happen for a while. But I think that adding a number_semiring class would be a step in the right direction, and it would be easy enough to make that change right now. - Brian On Wed, Jun 22, 2011 at 12:21 PM, Lawrence Paulson <[email protected]> wrote: > As I recall, the number class is for all types where numerals have a meaning. > Of course, it is a constituent of number_ring, to which many numeric types > belong, but not the naturals. > Larry > > On 22 Jun 2011, at 19:55, Florian Haftmann wrote: > >>> A more drastic solution would be to just get rid of the "number" class >>> altogether (its sole purpose seems to be so that you can have types >>> where numerals have a non-standard meaning) and have a single >>> definition of number_of that works uniformly for all types. >> >> This would indeed be helpful, but I guess the natural numbers are the >> show stopper. >> >> Of course we could also attempt to get rid of signed numerals ;-) >> >> Florian >> >> -- >> >> Home: >> http://www.in.tum.de/~haftmann >> >> PGP available: >> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de >> >> _______________________________________________ >> isabelle-dev mailing list >> [email protected] >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
