Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions



Hi Andreas,

> But this is probably not, what you wanted because the parenthesis ? around 
> a+b are missing, so set the precedence of the parameter to 66 (+ has 65 
> and * 70):
> notation (output) int ("_" [66] 1000)
> term "x * int (a + b) + f (int a)"
> (* output: "x * (a + b) + f a" *)

Wow, great! Works perfectly for me. I discoverd just a small flaw:

notation (output) int ("_" [66] 1000)
term "f (int (g a))"
(* output: "f g a" *)

notation (output) int ("_" [66] 999)
term "f (int (g a))" (* output: "f g a" *)
term "f (int (a + a))" (* output: "f ((a + a))" *)

Hence the parenthesis around "g a" is missing. When the precedence is
decreased the additional parenthesis is again shown. So it is probably
not enough as a replacement for the set-hidding in
"HOL/Library/OptionalSugar.thy".

Regards,
  Johannes






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.