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 : thm = |- (\x. ?y. x = a /\ y = b) y <=> > (?(y:'2). (y:'1) = a /\ (y:'2) = b)
Surely the ideal would be to avoid having ambiguous names by renaming as necessary? (though I agree that sufficient type information for disambiguation is also desirable) Roger Jones ------------------------------------------------------------------------------ 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
