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:

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:


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