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
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
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
Computed_Theorem thmname (ML code)
>>
>> Or …?
>>
>> Suggestions welcome.
>>
>> Michael
>>
>> From: "Chun Tian (binghe)"
mailto:binghe.l...@gmail.com>>
>> Date: Thursday, 3 January 2019 at
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
hus tempted to invent a Theorem
> analogue to map to it. My current feeling is to go for something like
> >>
> >> Theorem(calculated) thmname (ML code);
> >>
> >> Or
> >>
> >> Computed_Theorem thmname (ML code)
> >>
>> Suggestions welcome.
>>
>> Michael
>>
>> From: "Chun Tian (binghe)"
>> Date: Thursday, 3 January 2019 at 23:20
>> To: Makarius
>> Cc: Michael Norrish , hol-info
>> Subject: Re: [Hol-info]
g `save_thm` entrypoint has the same problem with requiring
>>> redundant typing of names. I’m thus tempted to invent a Theorem analogue to
>>> map to it. My current feeling is to go for something like
>>>
>>> Theorem(calculated) thmname (ML code);
>>>
&
;> Theorem(calculated) thmname (ML code);
>>
>> Or
>>
>> Computed_Theorem thmname (ML code)
>>
>> Or …?
>>
>> Suggestions welcome.
>>
>> Michael
>>
>> From: "Chun Tian (binghe)"
>> Date: Thursday
> From: "Chun Tian (binghe)"
> Date: Thursday, 3 January 2019 at 23:20
> To: Makarius
> Cc: Michael Norrish , hol-info
> Subject: Re: [Hol-info] New grammar of defining theorems?
>
> So the key is to make sure that they’re not disting
uted_Theorem thmname (ML code)
>
> Or …?
>
> Suggestions welcome.
>
> Michael
>
> From: "Chun Tian (binghe)"
> Date: Thursday, 3 January 2019 at 23:20
> To: Makarius
> Cc: Michael Norrish , hol-info
>
> Subject: Re: [Hol-info] New grammar of defining theo
On 03/01/2019 13:20, Chun Tian (binghe) wrote:
>
> I personally don’t like the keyword “Theorem” because I think many small
> theorems with 3 lines of tactics do not deserve the name “Theorem”. The
> correct way of using these conventions should be aligned with majority
> math books, which I
So the key is to make sure that they’re not distinguished internally by some
tools, and if some tools do, it’s their problems but HOL’s.
I personally don’t like the keyword “Theorem” because I think many small
theorems with 3 lines of tactics do not deserve the name “Theorem”. The correct
way
On 03/01/2019 11:23, Chun Tian (binghe) wrote:
> Hi Michael,
>
> thanks for fixing the bugs. (now I see why I can’t find its definition…)
>
> Going in this direction, have you considered adding also “Lemma” and
> “Corollary”? Internally they're equivalent with “Theorem”, but they could
>
Hi Michael,
thanks for fixing the bugs. (now I see why I can’t find its definition…)
Going in this direction, have you considered adding also “Lemma” and
“Corollary”? Internally they're equivalent with “Theorem”, but they could
literally help writers (and readers) identifying different levels
I see… thanks, but currently Moscow ML cannot compile that file [1], and I
can’t even find the definition of this new feature …
—Chun
[1] https://github.com/HOL-Theorem-Prover/HOL/pull/634
> Il giorno 02 gen 2019, alle ore 15:44,
> ha scritto:
>
> Dear Chun,
>
> This is indeed a new
Dear Chun,
This is indeed a new feature of the quotation filter. Its purpose is to keep
names consistent, and to reduce the amount of boilerplate typing that
script-writers have to generate.
It's as yet undocumented, but I hope to get to that soon.
Michael
On 2/1/19, 06:20, "Chun Tian
Hi,
(Happy New Year) I found the following code in src/patricia/sptreeScript.sml
(added in commit 2b78a8b8ac22b0686a5964a64f79fa8a8a17375e)
Theorem list_to_num_set_append
`!l1 l2. list_to_num_set (l1 ++ l2) = union (list_to_num_set l1)
(list_to_num_set l2)`
(Induct \\
18 matches
Mail list logo
