On 14 Aug 2012, at 00:30, Cris Perdue wrote:
>
>
> On Mon, Aug 13, 2012 at 6:05 PM, Bill Richter
> wrote:
>
>I prefer not to say that a type is a set, because the set of all
>things having a type is expressible as \x. T (or {x | T}.
>
> Cris, I'm tempted to go with Michael, who
Apologies for cross posting.
Regards,
Gergely
=
CALL FOR PARTICIPATION
28th International Conference on Logic Programming (ICLP 2012)
Theory and Practice of Logic Programming
Thanks, Konrad! Could you check to see if the HOL4 method of proving the IN_*
theorems is simpler than the HOL Light method? If it isn't, then maybe I
should be satisfied with what I came up with,following sets.ml
let IN_Interval = prove
(`! A B X. X IN open (A,B) <=> Between A X B`,
REW
Michael, I'm really grateful to you, as you cleared up my main problem:
> Now is my interpretation of my own code correct?
Your interpretation of what you've written seems fine to me.
That's great. I have to tell my audience of mathematicians what theorems HOL
Light is verifying, even
On 15/08/12 14:41, Bill Richter wrote:
> A counterexample to what you wrote:
> If you never use that [{ n + 1 | n > 6 }] notation, then it's
> certainly fine to just view { x | P x } as a fancy way of writing
> (λx. P x).
> I'll give 3 reasons below to indicate this isn't true for me
