I was hesitant to document anything before nailing down the final form of the
syntax. But it's clear that a fairly radical change like this one will need
good explanation.
It's particularly confusing because it's a form that cannot be explained in
terms of standard ML programming. (Our quotation syntax has the same problem.)
Michael
On 8/1/19, 17:08, "Jeremy Dawson" <jeremy.daw...@anu.edu.au> wrote:
On 8/1/19 4:49 pm, michael.norr...@data61.csiro.au wrote:
> I think you've misunderstood.
that's true, sorry.
> Here the advantage is quite clear and valuable: in the existing system,
you have to type the same string of symbols twice in order to avoid annoying
maintenance issues when theorems get moved. There's no utility in allowing
people to write things like
>
> val foo = save_thm("bar", ...)
>
> and it just leads to real pain.
>
there's certainly a discernible advantage in this particular case, I agree
> Slippery slope arguments cut no mustard.
>
Let's hope it's not the start of one. And do work out a way of getting
it into the online documentation (eg, in
HOL/help/src-sml/htmlsigs/idIndex.html)
Jeremy
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
