On 16/08/2012, at 14:57, Bill Richter <[email protected]> wrote:
> So I didn't solve your exercise, which maybe would have required me to
> understand your GSPEC and SET_SPEC, but I see the result should be true.
> Still, I don't admit I was wrong, as your phrase "fancy way of writing" isn't
> precise. What I meant is that {x|..} is clearly not syntactic sugar for (λx.
> ..). I would be happy if it was, so that {x|..} = (λx. ..) would be true
> without proof. It didn't occur to me that they were equal by a complicated
> proof.
Indeed, you wouldn't want { x | ...} to be syntactic sugar for (\x. ...)
because then otherwise innocuous lambda-expressions might get printed as set
comprehensions.
GSPEC and SET_SPEC are not "mine"; they're how HOL Light implements set
comprehensions. I have no idea how they work.
> As you see, I actually write with your symbols ∪, ∈, ∩, ∀, ∃, and use an
> Emacs preprocessor to turn these into the ordinary characters HOL Light uses.
> I'm glad to hear that HOL4, as well as Isabelle, uses these math symbols.
> Which one of you did it first, I wonder? It just hadn't occured to me to use
> your λ, but I will starting now! How hard would it be for HOL Light to be
> able to do this? Is that called supporting Unicode such tokens?
Isabelle supported “mathematical notation” a lot earlier than HOL4, but we do
it in rather different ways. I have no idea how HOL Light's
parsing/pretty-printing machinery works in general. I guess the thing to do
would be to try overloading a Unicode symbol to an ASCII one and to see what
happened... HOL Light has some sort of overloading mechanism I believe,
because I think it's possible to write x + y, for x of type :num or :real.
Michael
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
