Thanks to Konrad and Michael for their responses to my previous
question.
Here's another one. I'm not sure if it is a question about EVAL or a
pretty printing question. If I EVAL a function that has a finite domain
(especially a small one), I would like the function to be represented as
a set of pairs. However, EVAL tends to give unnecessarily complicated
terms when dealing with functions. For example,
Define `update f x y = \z. if z=x then y else (f z)`;
Define `not x = ~x`;
Now let's use update to morph not into the identity on bools.
EVAL ``update (update not T T) F F``;
I would like this to print the bool identity in some succinct manner
(something along the lines of [T |-> T, F |-> F])
Instead, EVAL gives the function as a nested if-then-else lambda
expression:
(\z. (if ~z then F else (if z then T else ~z)))
Things get worse if there are more updates. I tried using finite_maps
and |+ instead of update and got similar results, modulo notation. How
do I get EVAL to crunch a function with a finite domains down to a set
of pairs?
Thanks
-Jesse
-------------------------------------------------------------------------
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
