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:
> 
> https://en.wikipedia.org/wiki/Integer#Construction
> 
> 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.

  - Johannes





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