# Re: [isabelle] int vs. of_nat

The duplication is not intentional and it would be nice to eliminate it. One could choose either "ty :: 'a => ty" or "of_ty :: ty => 'a" as primitive (int::nat=>int should have been int::'a=>int) and relate them via (ty :: ty' => ty) = (of_ty' :: ty' => ty) for specif ty and ty'.
```
```
Function ty :: 'a => ty has the advantage of being the familiar one whereas of_ty is somewhat unusual. However, I gather that of_ty often allows to formulate polymorphic theorems whereas ty does not.
```
```
Maybe one could combine both advantages: of_ty is the primitive, but monomorphic instances are printed as ty (and ty is also allowed upon input).
```
Tobias

Brian Huffman wrote:
```
```Hello all,

```
Isabelle's standard library has two different coercions from the naturals to the integers: IntDef.thy defines "int::nat=>int" which is monomorphic, and Nat.thy defines "of_nat::nat=>'a" which coerces from naturals into an arbitrary semiring. At type "nat=>int" they both mean exactly the same thing (see lemma IntDef.int_eq_of_nat). The only difference is that they are each set up with different sets of simp rules.
```
```
My question is, why do we have both? If any of you have chosen to use one over the other, which one did you choose, and why?
```
```
Unless there is a compelling reason to keep both, I would propose to either make "int" an abbreviation for "of_nat::nat=>int", or just eliminate it altogether. Also, if users prefer the way the simplifier works with "int", then the simp rules for "of_nat" should be changed accordingly.
```
```
I could also ask the same thing about the overloaded function "real::'a=>real" from the HOL-Complex library, which is redundant with "of_nat::nat=>real" and "of_int::int=>real" at those types. Do we need separate constants for these?
```
- Brian
```
```

```

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