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 = |- (\x. ?y. x = a /\ y = b) y <=> (?(y:'2). (y:'1) = a /\ > (y:'2) = b)
HOL4's output is: > BETA_CONV ``(λx. ∃y. (x = a) ∧ (y = b)) y``; <<HOL message: inventing new type variable names: 'a, 'b>> val it = |- (λx. ∃y. (x = a) ∧ (y = b)) y ⇔ ∃y'. (y = a) ∧ (y' = b) : thm In addition, in emacs or vt100 terminals, it will colour the bound variables (x, y on the left, and y' on the right) green, and the free y, a and b blue (see attached screenshot). In the emacs terminal, you also get mouse-over tooltips identifying all the variables' types. The HOL message is another indication that there are multiple types involved. Michael
<<attachment: Screenshot.png>>
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Achieve unprecedented app performance and reliability What every C/C++ and Fortran developer should know. Learn how Intel has extended the reach of its next-generation tools to help boost performance applications - inlcuding clusters. http://p.sf.net/sfu/intel-dev2devmay
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
