Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy



On Tue, 21 May 2013, Gottfried Barrow wrote:

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.

Here are some more Q&A threads on nat vs. int, and the natural construction of int via quotients:

http://cstheory.stackexchange.com/questions/3772/why-naturals-instead-of-integers
http://mathoverflow.net/questions/29090/direct-construction-of-the-integers


	Makarius




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