The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 24/01/2014 21:27, Daniel Schepler wrote:
> Shouldn't it be easy to do something more generic by recursion on n
> instead of on v?  Something like:

Indeed, that works too. But that's still essentially the same technique,
and one ends up deconstructing and reconstructing the (unique) nat
argument, leading to a O(n) overhead.

(This is better behaved for extraction though, if targeted to produce
proof-irrelevant terms.)

PMP

Attachment: signature.asc
Description: OpenPGP digital signature