The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

>
> How do you measure nodes in a term?

I wrote an ML plugin which measures proofs and definitions and keeps
track of statistics (it helps when trying out different design
decisions or comparing tactics, in order to see the impact it has on
proof size in particular). The size of a term is just the size of the
term in the internal AST representation.

>
> It is said that machine integers are used to implement reductions involving
>
> Numbers.Cyclic.Int31
>
> Would using that further reduce overhead?

I have never used native integers before, but it would possibly help
yes, although the overhead is so small that I'm not sure how much of
an improvement that would represent.

S.
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06