on 16/5/11 10:14 AM, Roger Bishop Jones wrote:
> Even though I am not particularly concerned with
> trustworthyness (at your level) it is still a awkwardness in
> my own use of ProofPower that I cannot get unambiguous and
> concise theory listings, partly because I get either too
> much or too lit
On Monday 16 May 2011 07:52, Mark wrote:
> ? [rbj]
> > Surely the ideal would be to avoid having ambiguous
> > names by renaming as necessary?
>
> I would think so, yes. But I'm talking about the pretty
> printer:
of course, I mistook the issue at stake.
> given any internal representation of
> Surely the ideal would be to avoid having ambiguous names by
> renaming as necessary?
I would think so, yes. But I'm talking about the pretty printer: given any
internal representation of a theorem (with whatever confusing forms of
overloading that it has), ensuring that the pretty printer outp
On 16/05/11 16:10, Roger Bishop Jones wrote:
> On Sunday 15 May 2011 15:08, Mark wrote:
>> In fact HOL Zero is the only HOL system with a pretty
>> printer specially designed to avoid all possible
>> confusing results like that. For this situation, it
>> returns Rob's "ideal output":
>>
>> # bet
On Sunday 15 May 2011 15:08, Mark wrote:
> In fact HOL Zero is the only HOL system with a pretty
> printer specially designed to avoid all possible
> confusing results like that. For this situation, it
> returns Rob's "ideal output":
>
> # beta_conv `(\x. ?y. x = a /\ y = b) y`;;
> val it : t
> HOL4's output is:
>
>> BETA_CONV ``(λx. ∃y. (x = a) ∧ (y = b)) y``;
> <>
> val it =
> |- (λx. ∃y. (x = a) ∧ (y = b)) y ⇔ ∃y'. (y = a) ∧ (y' = b)
> : thm
Yes the HOL4 pretty printer is better than HOL Light's in various respects.
So is ProofPower's (but not in this respect). But neither distingu
On 16/05/11 00:08, "Mark" wrote:
> In fact HOL Zero is the only HOL system with a pretty printer specially
> designed to avoid all possible confusing results like that. For this
> situation, it returns Rob's "ideal output":
>
> # beta_conv `(\x. ?y. x = a /\ y = b) y`;;
> val it : thm = |- (\
In fact HOL Zero is the only HOL system with a pretty printer specially
designed to avoid all possible confusing results like that. For this
situation, it returns Rob's "ideal output":
# beta_conv `(\x. ?y. x = a /\ y = b) y`;;
val it : thm = |- (\x. ?y. x = a /\ y = b) y <=> (?(y:'2). (y:'1)
On 13 May 2011, at 08:11, hao deng wrote:
> Hi, there:
>I'm a new user of hol-light and I find the following thing strange :
>
> # BETA_CONV `(\x. ?y. x = a /\ y = b) y`;;
> Warning: inventing type variables
> val it : thm = |- (\x. ?y. x = a /\ y = b) y <=> (?y. y = a /\ y = b)
>
> the ?y
Hi, there:
I'm a new user of hol-light and I find the following thing strange :
# BETA_CONV `(\x. ?y. x = a /\ y = b) y`;;
Warning: inventing type variables
val it : thm = |- (\x. ?y. x = a /\ y = b) y <=> (?y. y = a /\ y = b)
the ?y is not renamed in the substitution , is this a bug ?
or am
10 matches
Mail list logo
