To follow up on Thomas' post, you can easily write a tactical that will do
such counting. In
the following I print out the number, but you could also store it in a
reference cell, as Thomas
does.
fun COUNT_TAC tac g =
let val res as (sg,_) = tac g
val _ = print
Hi Matthias,
I'm not aware of an easy way. Moreover, for me it is unclear how to
count subgoals. I could well imagine that one wants to count only
"interesting ones", i.e. ignore trivial ones like "Cases_on `x:num` >>
ASM_REWRITE_TAC[...]", where the case for "0" is automatically discarded.
One
Hi,
I'm working on a proof that produces many subgoals due to a rather
complex case-splitting structure. To see, if some changes to the proof
increase or decrease the complexity, I'd like to know how many subgoals
are produced and solved in the whole proof.
So, is there any way to find out
