Tony Johnson wrote:
> Is there a way to turn off the pretty printing of specialized
> notation, while still having the parser recognize it?
Yes!
> For example, what I want to do is prove the equivalency of 2 sets.
> (--`{1;2} = {x | (x = 1) \/ (x = 2)}`--)
> Can I enter in above term in the interactive prompt, and have the
> display show it in it's native term form? So it would look something
> like this..
> (--`(1 INSERT (2 INSERT EMPTY)) = ???`--))
In HOL4, this is covered in the FAQ (see hol.sf.net).
Unfortunately, there is a bug on this example. If you do
- print_term_by_grammar listTheory.list_grammars
``{1;2} = { x | (x = 1) \/ (x = 2)}``;
you get
pred_set$INSERT 1 (pred_set$INSERT 2 pred_set$EMPTY) =
{x | (x = 1) \/ (x = 2)}
as output.
(If you used boolTheory.bool_grammars you'd see the internal structure
of the numerals too.)
The GSPEC is handled specially by the pretty-printer so it always
works regardless of the grammar. Until that's fixed, you can often
get a good idea of the underlying structure if you use dest_term:
- dest_term ``{x | (x = 1) \/ (x = 2) }``;
> val it = COMB(``GSPEC``, ``\x. (x,(x = 1) \/ (x = 2))``) : lambda
You can set the pretty-printing function used all the time to be
whatever you like with
Parse.set_term_printer
The default printer is thus something like
print_term_by_grammar (type_grammar(), term_grammar())
where the function calls to get the grammar values are made each time
in order to have the printing function change its behaviour as the
global grammar variables change.
Michael.
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
