Email Gateway (Aug 18 2022 at 12:54): Email Gateway (Aug 18 2022 at 12:54):From: Johannes Hoelzl <hoelzl@in.tum.de>
I want to hide the "int", "nat" and "real" conversion functions when
Isabelle outputs an term. So that a term like
"nat (x * int y - f (int z))" gets written as "x * y - f z" human users
are usually capable of interfering the correct conversion functions.
First I tried to just add a translation:
translations
"N" <= "of_nat N" (* "int" do not work, it is represented as "of_nat" internally *)
term "int 1 + 2"
(* output: "2" HUH! *)
This breaks the entire output process! Is this a bug in the pretty
printer or should I just not add this translation. In OptionalSugar the
same is done with the "set :: 'a list => 'a set" conversion function!
As alternative I'm currently using a notation:
notation (output) int ("_" 70)
term "x * int (a + b) + f (int a)"
(* output: "x * (a + b) + f (a)" *)
This nearly works, but I don't get rid of the parenthesis around the
function parameter. I tried several other precedencies but no one
worked. There are parenthesis around the function parameter or the
parenthesis around the addition are missing.
Has anyone a solution to this problem?
Regards,
Johannes Hölzl
Last updated: May 03 2024 at 08:18 UTC