| Compare (_, term) -> countterm (current_size + 7) term
| Constructor (_, n) -> current_size + 12
| Contradiction _ -> current_size + 13
- | Cut (_, term) -> countterm (current_size + 4) term
+ | Cut (_, ident, term) ->
+ let id_size =
+ match ident with
+ None -> 0
+ | Some id -> String.length id + 4
+ in
+ countterm (current_size + 4 + id_size) term
| DecideEquality _ -> current_size + 15
| Decompose (_, term) ->
countterm (current_size + 11) term
Box.indent(ast2astBox term)])
| Constructor (_,n) -> Box.Text ([],"constructor " ^ string_of_int n)
| Contradiction _ -> Box.Text([],"contradiction")
- | Cut (_, term) ->
- Box.V([],[Box.Text([],"cut");
- Box.indent(ast2astBox term)])
| DecideEquality _ -> Box.Text([],"decide equality")
| Decompose (_, term) ->
Box.V([],[Box.Text([],"decompose");