I think you've misunderstood. One form maps to store_thm; the other maps to
save_thm. In both cases the name is likely to be fresh, just as the names
passed to store_thm and save_thm are usually fresh. (If they're not, the
underlying SML functions emit warning messages.)
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.
Slippery slope arguments cut no mustard.
Michael
On 8/1/19, 15:09, "Jeremy Dawson" <jeremy.daw...@anu.edu.au> wrote:
This summary seems to make it clear that this new feature achieves very
little, with the following costs:
- it gives users yet something else (as if there isn't already enough!)
to lookup in the documentation, or ask questions about
- it's positively confusing, in that
"Theorem name ... " has totally different meanings, depending on which
case applies (eg, in one case, name must already exist, in the other, it
ought not to already exist)
This idea looks like the start of the path followed in Isabelle and Coq,
of having a multitude of commands, some with a multitude of variants (eg
optional arguments) with no coherent consistent grammar rules - just so
that the user doesn't need to type a few punctuation symbols.
Jeremy
On 8/1/19 2:41 pm, Konrad Slind wrote:
> Isn't it clear just from the form?
>
> Theorem name quote (ML) --> val name = Q.store_thm(name,quote,ML)
> Theorem name (ML) --> val name = save_thm(name,ML)
>
>
_______________________________________________
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
