[isabelle-dev] »real« considered harmful

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Jun 5 23:22:27 CEST 2015

> Why do we need abbreviations such as these?
> abbreviation real_of_nat :: "nat \<Rightarrow> real”
>   where "real_of_nat \<equiv> of_nat"
> abbreviation real_of_int :: "int \<Rightarrow> real”
>   where "real_of_int \<equiv> of_int"
> abbreviation real_of_rat :: "rat \<Rightarrow> real”
>   where "real_of_rat \<equiv> of_rat"
> abbreviation complex_of_real :: "real \<Rightarrow> complex"
>   where "complex_of_real \<equiv> of_real"

The deeper reason why these have been introduced is that such
conversions of type T => 'a::c can be difficult to write in presence of
type ambiguities.  If you need more special types, you can do barely
anything else than writing »(of_foo x :: T)« which clutters readability.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150605/9a8f6734/attachment.sig>

More information about the isabelle-dev mailing list