| ElimType (_, term) -> countterm (current_size + 10) term
| Exact (_, term) -> countterm (current_size + 6) term
| Exists _ -> current_size + 6
- | Fold (_, kind, term) ->
- countterm (current_size + 5) term
| Fourier _ -> current_size + 7
| Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
| Injection (_, term) ->
| LetIn (_, term, ident) ->
countterm (current_size + 5 + String.length ident) term
| Reflexivity _ -> current_size + 11
- | Replace (_, t1, t2) ->
- let size1 = countterm (current_size + 14) t1 in (* replace, with *)
- countterm size1 t2
| Right _ -> current_size + 5
| Ring _ -> current_size + 4
| Split _ -> current_size + 5
Box.V([],[Box.Text([],"exact");
Box.indent(ast2astBox term)])
| Exists _ -> Box.Text([],"exists")
- | Fold (_, kind, term) ->
- Box.V([],[Box.H([],[Box.Text([],"fold");
- Box.smallskip;
- Box.Text([],string_of_kind kind)]);
- Box.indent(ast2astBox term)])
| Fourier _ -> Box.Text([],"fourier")
| Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
| Intros (_, num, idents) ->
Box.Text([],"=")]);
Box.indent (ast2astBox term)])
| Reflexivity _ -> Box.Text([],"reflexivity")
- | Replace (_, t1, t2) ->
- Box.V([],
- (pretty_append
- [Box.Text([],"replace")]
- t1)@
- (pretty_append
- [Box.Text([],"with")]
- t2))
| Right _ -> Box.Text([],"right")
| Ring _ -> Box.Text([],"ring")
| Split _ -> Box.Text([],"split")
let rec tactical2box = function
| Tactic (_, tac) -> tactic2box tac
-(*
- | Command cmd -> (* TODO dummy implementation *)
- Box.Text([], TacticAstPp.pp_tactical (Command cmd))
-*)
-
- | Fail _ -> Box.Text([],"fail")
| Do (_, count, tac) ->
Box.V([],[Box.Text([],"do " ^ string_of_int count);
Box.indent (tactical2box tac)])
- | IdTac _ -> Box.Text([],"id")
| Repeat (_, tac) ->
Box.V([],[Box.Text([],"repeat");
Box.indent (tactical2box tac)])