On 25/10/12 09:27, Vincent Aravantinos wrote: > It was actually easy to define mine, see > <http://users.encs.concordia.ca/~vincent/Software_files/q.ml> if interested.
> Ex: > The goal: > # g `!x:real. P x ==> ?y. P y` > can be reduced by the following tactic: > # e (REPEAT STRIP_TAC THEN Pa.EXISTS_TAC "x") > Its standard equivalent would be the following, which requires a type > annotation: > # e (REPEAT STRIP_TAC THEN EXISTS_TAC `x:real`) It can also be useful (in the EXISTS_TAC scenario, and in others too) to have the goal-informed parsing know about the expected type of the whole term. For example, if the goal is ?x:real. P x then the string being passed to the better version of EXISTS_TAC should have type real if the tactic is to succeed. In HOL4, in the above situation you might write Q.EXISTS_TAC `0`, for example. If I remember right, that’s not such an issue in HOL Light because the numerals are not overloaded, so you’d naturally be writing &0 anyway (though if the integers are also in scope, presumably &0 might have type real or int and the problem reappears). The same problem appears with genuine polymorphism: if the goal is ?l:num list. P l and you want to provide the empty list as a witness, it’s nice to be able to write Q.EXISTS_TAC `[]` rather than EXISTS_TAC ``[]:num list``. Even in SUBGOAL_THEN we assert that the type of the quotation had better be bool. Best, Michael ------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_sfd2d_oct _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
