coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ascii module

From: Tom Prince <tom.prince AT ualberta.net>
To: Stéphane Lescuyer <stephane.lescuyer AT inria.fr>, Brandon Moore <brandon_m_moore AT yahoo.com>
Cc: AUGER Cedric <Cedric.Auger AT lri.fr>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Ascii module
Date: Fri, 04 Mar 2011 17:04:31 -0500

On 2011-03-04, Stéphane Lescuyer wrote:
> >
> > 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.

Is this available anywhere?

Tom

Re: [Coq-Club] Ascii module, (continued)