On Sat, May 5, 2012 at 11:43 PM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> The first thing I did with your Mizar code was to remove them.
>
> Wow, you were really working, I feel guilty. The file joe.miz has the
> fancy character turned into Mizar, for, ex, st, implies, etc.
>
> | It sure makes the code more readable.
>
> That's a matter of opinion.
>
> It's definitely my opinion, and I know when I came to it. I was
> staring at my proof of Gupta's theorem and I said to myself, I can't
> read this, I have no idea what I'm writing. After I wrote my Emacs
> code and stuck in (the top-level bits?) ⇒, ¬, ∨, ∧, ≡, ∀, ∃ and ⇔, it
> was so much more readable. That's the way mathematicians actually
> write, of course, so it's hard for me to read anything else.
>
> I would discourage it and advise you to set up some additional
> interface layer.
>
> I'll do it your way, you're the expert. What do you mean? Something
> like my Emacs stunt to rewrite the file before compiling it? Is there
> a clean way to do that? I wasn't too happy with my solution.
>
You may be interested to know that in HOL4, every constant has an ASCII
name, but some constants also have a Unicode name. So for example
implication is "==>", but it also has the Unicode name "⇒". You have the
option of making the printer print back ASCII or Unicode, and the parser
will accept either.
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
