Thanks, Vince! Can you remind me about your module & tactics that improve readability, with fewer type annotations?
I generally prefer the usual tactic style rather than the declarative style. I don't tend to think these words are too helpful. The important words are readable and powerful (rather than declarative and procedural), and we want both. My code hol_light/Examples/inverse_bug_puzzle_tac.ml uses tactics, and I think the proofs are quite readable if you first turn it into an interactive proof, evaluate it, and look at the output. It's very similar to hol_light/Examples/inverse_bug_puzzle_miz3.ml, which is however a lot more readable if you just read the code. So what I want is to make inverse_bug_puzzle_tac.ml more readable without interactive/evaluation. Isn't that the sort of thing you're doing? -- Best, Bill ------------------------------------------------------------------------------ Minimize network downtime and maximize team effectiveness. Reduce network management and security costs.Learn how to hire the most talented Cisco Certified professionals. Visit the Employer Resources Portal http://www.cisco.com/web/learning/employer_resources/index.html _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
