on 16/5/11 10:14 AM, Roger Bishop Jones <[email protected]> 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 little type information, or because of the > effects of type abbreviations and aliasing. > It sounds as if HOL4 and HOL zero have made some > improvements in these areas.
Yes, the main reason for HOL Zero not supporting type abbreviations or aliasing (other than boolean equality) is to keep things simple and avoid confusion for the user. I've gone to great lengths to try to ensure no ambiguity whatsoever in anything outputted by the pretty printer (assuming knowledge of all declared constants, type operators and fixity settings). I was bitten too many times in the past by subtle problems in large projects, misreading ambiguous output that I subconsciously assumed meant "the obvious". 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
