The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Le 03/03/2011 01:45, AUGER Cedric a écrit :
> > Do people out there actually use inductives with zillions (or, say,
> > hundreds) of constructors ? I'm quite curious about it.
> I don't think anybody does that, but if one day some people want to do
> benchmarks on coq, it could be a thing to try!
I don't think that this is so uncommon. For instance, processors often 
have dozens or hundreds of instructions. The ARMv6 processor has 147 
32-bits instructions and 73 16-bits instructions... Many term rewrite 
systems in the Termination Problem Data Base have dozens of function 
symbols. Some have more than several hundred symbols. So, I would say 
that hundreds of constructors is not so uncommon. Now, thousands of 
constructors is perhaps more uncommon. Frederic.