*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 22 Jan 2009 08:03:51 -0800*In-reply-to*: <1232558290.27529.20.camel@macbroy24.informatik.tu-muenchen.de>*References*: <1232558290.27529.20.camel@macbroy24.informatik.tu-muenchen.de>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

Try the following: translations "N" <= "CONST of_nat N" "N" <= "CONST int N"

In your example, you entered translations "N" <= "of_nat N" and the system thought you meant translations "N" <= "M N" which explains why "int 1 + 2" would print out as just "2".

- Brian Quoting Johannes Hoelzl <hoelzl at 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

**References**:**[isabelle] Hidding the "int", "nat" and "real" conversion functions***From:*Johannes Hoelzl

- Previous by Date: [isabelle] "The QED Project"
- Next by Date: [isabelle] Isabelle document preparation
- Previous by Thread: Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions
- Next by Thread: [isabelle] parameters of function definitions and scope of constants
- Cl-isabelle-users January 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list