> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
