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 look forward to the eventual PR!
Micahel
On 8/1/19, 02:33, "Chun Tian (binghe)" wrote:
Beside, there’re two other benefits:
1) Hurd’s original elegant long proof of CARATHEODORY is now preserved in
old_measureTheory.
2) Coble’s “dining cryptographers” work
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
You can’t/don’t want to write a regular expression to distinguish these by
matching the entirety of the goal and tactic.
Michael
From: Konrad Slind
Date: Tuesday, 8 January 2019 at 14:41
To: "Norrish, Michael (Data61, Acton)"
Cc: hol-info
Subject: Re: [Hol-info] New grammar of defining
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
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)
On Mon, Jan 7, 2019 at 8:34 PM wrote:
> Forward and backward give us nice terminology, thanks! It may also be
>
Forward and backward give us nice terminology, thanks! It may also be possible
to have the quotation filter figure things out by looking for the
left-parenthesis that is required to follow the name in the forward case. I
may play with that.
Michael
On 8/1/19, 12:38, "Chun Tian (binghe)"
You are close. Use MAP.
And please don’t use a mailing list to do assignments.
Michael
From: 幻＠未来 <849678...@qq.com>
Date: Tuesday, 8 January 2019 at 12:49
To: hol-info
Subject: [Hol-info] assignment
The following data types are defined in HOL4.
val _ = Datatype `
The following data types are defined in HOL4.
val _ = Datatype ` coordinate = <|
x_axis: real;
y_axis: real; z_axis: real
I quote the beginning of the 2nd paragraph of Chapter 4 (Goal Directed Proof:
Tactics and Tacticals) in The HOL System DESCRIPTION:
"Even with recourse to derived inference rules, it is still surprisingly
awkward to work
*forward*, to find a chain of theorems that culminates in a desired
The following data types are defined in HOL4.
val _ = Datatype ` coordinate = <|
x_axis: real;
y_axis: real; z_axis: real
Hmmm, well… all theorems are essentially *derived* from earlier theorems or
axioms, thus it seems (to me) that the word “derived” still doesn’t capture the
characterization of “save_thm” from “store_thm”. But the word “dervied” makes
more senses than previous “calculated” as “save_thm”’s body
Indeed, they are both calculated. In one, you state the desired end-state and
head towards it with a tactic. In the other, you transform existing theorems
with rules of inference and derive a final statement (hence the good practice,
which you mentioned, of putting the statement into a
Your problem statement doesn’t make sense. Why do you say “*the* ch in the
pop”? Surely a pop may contain multiple ch values.
As I said before, it seems as if you should try to write your program in SML
(or Haskell, or OCaml) first. Then you might think about formalising it in
HOL. If you
The following data types are defined in HOL4.val _ =
Datatype ` coordinate = <|
x_axis: real; y_axis: real;
z_axis: real
Beside, there’re two other benefits:
1) Hurd’s original elegant long proof of CARATHEODORY is now preserved in
old_measureTheory.
2) Coble’s “dining cryptographers” work (example/diningcryptos) can also be
fixed (in the future) under old_measureTheory and old_probabilityTheory,
because his
Hi Micheal,
thanks for your trust. Now I’ve done the following solution for preserving
some backwards compatibilities:
My goal is to make minimal efforts to make sure that Hurd's Miller-Rabin work
(examples/miller) can still build after my PR.I found that, the code in
“miller” depends
Hi Michael,
Thanks, now I see your points: if it’s really a “lemma”, then there’s no need
to export it, thus `Q.prove` (or `prove`) should just do the job.
Among the two syntactic sugars, I personally like your first version
(Theorem(calculated) …), because it emphasized that, a `Theorem`
> Il giorno 07 gen 2019, alle ore 01:52, Waqar Ahmad <12phdwah...@seecs.edu.pk>
> ha scritto:
>
> Hi Chun,
>
> I think it’s better to let HOL maintainers to decide if we should keep the
> old version (14,700 lines) in “examples”, e.g. “examples/old-probability”. I
> personally don’t like
20 matches
Mail list logo
