On 04/30/2013 10:24 AM, Bill Richter wrote: > I wrote my type annotation reducing versions of EXISTS_TAC and X_GEN_TAC, and > cleaned up the code, with > > let (make_env: goal -> (string * pretype) list) = > fun (asl,w) -> map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var) > (freesl (w::(map (concl o snd) asl)));; > > let parse_env_string env s = (term_of_preterm o retypecheck env) > ((fst o parse_preterm o lex o explode) s);; > > let (subgoal_THEN: string -> thm_tactic -> tactic) = > fun stm ttac (asl,w) -> > let wa = parse_env_string (make_env (asl,w)) stm in > let meta,gl,just = ttac (ASSUME wa) (asl,w) in > meta,(asl,wa)::gl,fun i l -> PROVE_HYP (hd l) (just i (tl l));; > > let (exists_TAC: string -> tactic) = > fun stm (asl,w) -> let env = make_env (asl,w) in > EXISTS_TAC (parse_env_string env stm) (asl,w);; > > let (X_gen_TAC: string -> tactic) = > fun svar (asl,w) -> > let vartype = (snd o dest_var o fst o dest_forall) w in > X_GEN_TAC (mk_var (svar,vartype)) (asl,w);;
Hi Bill, for your info, this is also done in my Q-like module: https://github.com/aravantv/HOL-Light-Q (as well as many other tactics). V. -- Vincent Aravantinos Postdoctoral Fellow, Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent ------------------------------------------------------------------------------ Introducing AppDynamics Lite, a free troubleshooting tool for Java/.NET Get 100% visibility into your production application - at no cost. Code-level diagnostics for performance bottlenecks with <2% overhead Download for free and get started troubleshooting in minutes. http://p.sf.net/sfu/appdyn_d2d_ap1 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
