The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Andreas Lundblad a écrit :
> Rewriting it as a [fun] worked fine. Thanks.
> 
> My original problem was actually not on lists, but on a data type with
> a large number of constructors. I didn't want to use [destruct] since
> it generated a lot of cases, which I thought was completely
> unnecessary since the required fact ([nth 2 l 7] in the above case)
> was independent of the constructor.

As Adam said, you have to do a case analysis to "unfold" a fixpoint, so
it's better not to use fix if possible.

However, you can also use "Function" (see documentation) to define your
fixpoint. This will generate an equation lemma that you can use to
rewrite the fixpoint call into its body.


Cheers,

-- 
Stéphane