The syntax is nice, but I would interpret "_⇩ℕ" not as of_nat but as into nat, or more specifically I would read: _⇩ℝ == real _.
- Johannes Am Freitag, den 05.06.2015, 23:58 +0200 schrieb Florian Haftmann: > Hi again, > > after I first iteration of discussion I see a list of three requirements: > > 1. Conversions can be written succinctly. > 2. Conversions are printed succinctly. > 3. Conversions are unique, there are no accidental equivalences which > require explicit conversions. > > Concerning (1), my guess indeed is the implicit conversions should do > the job. There is the borderline case with required explicit type > annotations (»of_nat n :: rat«) which is currently handled by distinct > abbreviations, but these could be dropped. > > (2) is not so trivial if you want to make sure that the printed terms > are compact but still complete in the sense that they are invariant > under copy-and-paste. I think of_nat/of_int/of_rat is fine, but > real_of_int etc. is definitely not. Anyway, like in (1) these > abbreviations might be entirely superfluous. The disadvantage of the > algebraic conversions is that the do not tell what the result type is -- > which is usually the more important information, since the argument > type's is usually easily inferred. Maybe suitable symbol syntax can > help here. > > Below I made some experiments how fancy symbol syntax could look like, > but I am still lacking a conclusive idea. > > (3) Everything has been said about this already. > > So, I would suggest we spend thoughts how *printing* of > of_foo-Conversions can be improved with reasonable means (2). We are > still at the beginngin… > > Cheers, > Florian > > > notation of_nat ("_⇩ℕ" [999]) > > notation of_int ("_⇩ℤ" [999]) > > notation of_rat ("_⇩ℚ" [999]) > > > > term "rep_real (of_nat (Suc n) + of_int (k div l))" > > thm of_nat_diff > > > > notation real_of_nat ("of'_nat⇩ℝ") > > notation real_of_int ("of'_int⇩ℝ") > > notation real_of_rat ("of'_int⇩ℚ") > > > > term "rep_real (of_nat (Suc n) + of_int (k div l))" > > thm of_nat_diff > > > > notation of_nat ("of'_ℕ") > > notation of_int ("of'_ℤ") > > notation of_rat ("of'_ℚ") > > > > term "rep_real (of_nat (Suc n) + of_int (k div l))" > > thm of_nat_diff > > > > notation real_of_nat ("ℝ'_of'_ℕ") > > notation real_of_int ("ℝ'_of'_ℤ") > > notation real_of_rat ("ℝ'_of'_ℚ") > > > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev