[isabelle-dev] »real« considered harmful

[Florian Haftmann]

> 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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>