> 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 output faithfully represents that internal representation, so as not to mislead the user. This is the pertinent question when it comes to theorem prover trustworthiness (other than the logical soundness of internal deductions and the architecture of the inference kernel). Mark. ------------------------------------------------------------------------------ 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
