Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
Am Dienstag, den 21.05.2013, 22:23 -0500 schrieb Gottfried Barrow:
> It'd be interesting to know if it's common these days for other
> languages to use the classic definition of the integers as equivalence
> classes like you did with Int.thy:
> It seems it's common for the natural numbers to be built using the
> successor function, but I'm guessing it's not so common for the integers
> to be equivalence classes.
In my experience it is quite the other way round. The first semesters
mathematics course I attended introduced the integers, the rational
numbers and the real numbers as equivalence classes. Only the natural
numbers and the complex numbers where introduced like a datatype.
This archive was generated by a fusion of
Pipermail (Mailman edition) and