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

```On 5/22/2013 1:58 AM, Johannes Hölzl 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.
```
```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,

```
Thanks for your comment. I was comparing the formal, textbook construction of the integers, as in what you're listing, to concrete implementations of integers in programming languages, such as Coq, Isabelle/HOL, Haskell, or any other language, old or new, but especially new.
```
```
I'm speculating that this ability of Isabelle/HOL to define integers as equivalence classes is special, and that it takes a special foundation in a language to be able to do it, and that most languages don't have the foundation to be able to do it in a practical way.
```
```
But I wouldn't know. This is the first time I've ever delved into the low-level internals of a programming language, but defining an integer as a set, in particular as an equivalence class, seems like it requires some clever and sophisticated foundational code.
```
```
First, a person would simply know how it could be done at all. But that's not enough; their code would have to perform reasonably fast.
```
```
I wouldn't know where to begin, and I'm sure any initial discovery of mine on how to do it would be so slow, it would be useless.
```
```
All that to say, I'm guessing that Isabelle/HOL is pretty special in this ability to achieve a textbook definition of the integers. But I try not to become dogmatic about things I don't know about, and it could be that it's very common for programming languages to implement integers as equivalence classes.
```
Regards,
GB

```

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