]
;;
-let apply_tac (s,n,t) = exact_tac (s,n,Ast.Appl [t; Ast.Implicit `Vector]);;
+let apply_tac (s,n,t) =
+ let t = Ast.Appl [t; Ast.Implicit `Vector] in
+ exact_tac (s,n,t)
+;;
type indtyinfo = {
rightno: int;
}
;;
-let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
+let analyze_indty_tac ~what indtyref =
+ distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
let status, what = disambiguate status what None (ctx_of goalty) in
let status, ty_what = typeof status (ctx_of what) what in
exec id_tac status goal)
;;
-let elim_tac ~what ~where =
+let elim_tac ~what:(txt,len,what) ~where =
+ let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
let indtyinfo = ref None in
let sort = ref None in
let compute_goal_sort_tac = distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
let status, goalsort = typeof status (ctx_of goalty) goalty in
+ let goalsort = fix_sorts goalsort in
sort := Some goalsort;
exec id_tac status goal)
in
"_rect_" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] sort
| _ -> assert false
in
- let holes =
- HExtlib.mk_list (Ast.Implicit `JustOne)
- (ity.leftno+1+ ity.consno + ity.rightno) in
let eliminator =
let _,_,w = what in
- Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
+ Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
in
exact_tac ("",0,eliminator) status) ])
;;
| _ -> assert false
in
let name =
- match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq" ^ suffix
+ match dir with
+ `LeftToRight -> "eq" ^ suffix ^ "_r"
+ | `RightToLeft -> "eq" ^ suffix
in
block_tac
[ select_tac ~where ~job:(`Substexpand 1) true;
instantiate status goal t
;;
-let cases_tac ~what ~where =
+let cases_tac ~what:(txt,len,what) ~where =
+ let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
let indtyinfo = ref None in
atomic_tac
(block_tac [
if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
;;
+let constructor ?(num=1) ~args status goal =
+ if num < 1 then fail (lazy "constructor numbers begin with 1");
+ let gty = get_goalty status goal in
+ let status, (r,_,_,_) = analyse_indty status gty in
+ let ref = NReference.mk_constructor num r in
+ let t =
+ if args = [] then Ast.NRef ref else
+ Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector]
+ ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args))
+ in
+ exec (apply_tac ("",0,t)) status goal
+;;
+
+let constructor_tac ?num ~args = distribute_tac (constructor ?num ~args);;
+
let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
let gty = get_goalty status goal in
let eq status ctx t1 t2 =