Le 24/10/12 18:50, Michael Norrish a écrit : > 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. Hi Michael,
Indeed, I had not think of this. Thanks! I uploaded a new version taking this into account for EXISTS_TAC and SUBGOAL_THEN. V. ------------------------------------------------------------------------------ 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
