- let count = T.count_steps 0 ast in
- let text = Printf.sprintf "tactics: %u" count in
- T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
- | _ ->
- failwith "not a theorem"
+ let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
+ let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in
+ T.Statement (`Theorem, Some s, t, None, "") :: ast @ [T.Qed text]
+ | C.AConstant (_, _, s, Some v, t, [], pars) when is_definition pars ->
+ [T.Statement (`Definition, Some s, t, Some v, "")]
+ | C.AConstant (_, _, s, None, t, [], pars) ->
+ [T.Statement (`Axiom, Some s, t, None, "")]
+ | _ ->
+ failwith "not a theorem, definition, axiom"