On 5 Jun 2015, at 22:22, Florian Haftmann
<florian.haftm...@informatik.tu-muenchen.de> wrote:
>
>> 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.
OK — but that’s no reason to introduce “real” as another way to write these
coercions, while introducing precisely the sort of type ambiguity that is the
root of such problems.
Conceivably we could introduce a prefix syntax for type constraints, e.g.
[:real:]of_nat k
I’d find such a thing useful from time to time.
Larry
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
