Concerning the previous discussion, I believe there was no talking at cross
purposes,
as prior to your new reference to [Cohn, 1989] we were discussing within the
realm of mathematics only.
Especially the design of Mark's HOL Zero, which was chosen as an example by
Peter and Makarius,
focuses
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