> 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/5/2011 1:16 πμ, hao deng wrote:
> let str_IND, str_RECUR = define_type "str = Str (int list)";;
>
> let expr_IND, expr_RECUR = define_type
> " expr = Lit num
> |Var str
> |Plus expr expr
> |Times expr expr ";;
>
> let cmd_IND, cmd_REC = define_type
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 = |- (\
Hello there:
I have a small piece of code which I don't know where is the problem.
===
let str_IND, str_RECUR = define_type "str = Str (int list)";;
let expr_IND, expr_RECUR = define_type
" expr = Lit num
|Var str
|Plu
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)
Hi, there:
Is there any checkpoint software on mac ? like ckpt of zandy ?
Thanks in advance.
--
Achieve unprecedented app performance and reliability
What every C/C++ and Fortran developer should know.
Learn how Intel
