The Coq mailing list

[Edwin Brady <E.C.Brady AT durham.ac.uk>]

If I have a dependent type such as, for example, the following:

Inductive natvect:nat->Set :=
  empty:(natvect O) |
  cons:(n:nat;v:(natvect n))(item:nat)(natvect (S n)).

And I try to prove a simple theorem with an object of this type in the
goal, such as:

Lemma test:(w:(natvect O))(w=empty).

I would expect to be able to prove this by case analysis on w - there is
only one constructor which can give us a natvect O. However, Case,
Induction and NewInduction on w all give the following error message:

"Error: Cannot solve a second-order unification problem"

Is there another way to approach this problem?

Thanks,
Edwin.



-------------------
To unsubscribe, mail 
coq-club-request AT pauillac.inria.fr
Bug reports: http://coq.inria.fr/bin/coq-bugs
Coq-Club Archives: http://coq.inria.fr/mailing-lists/coqclub/