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



Hi Johannes,

> notation (output) int ("_" 70)
> term "x * int (a + b) + f (int a)"
> (* output: "x * (a + b) + f (a)" *)

I don't know whether you can do it with a translation, but your notation works if you use the precedence 1000. This is then as strong as function application, so no parenthesis are printed any more:

term "x * int (a + b) + f (int a)"
(* output: "x * a + b + f a" *)

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" *)

Regards,
Andreas





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