Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Problem with rewriting

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with rewriting


chronological Thread 
  • From: dimitrisg7 <dvekris AT hotmail.com>
  • To: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Problem with rewriting
  • Date: Sun, 7 Jun 2009 05:11:38 -0700 (PDT)
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi again!

I would like to get "Var" given by Hypothesis e in the following example.

 e : exists v : Var, f_expr_IL v = nth j el dE 
  ============================
   Var

Writing "elim e" I get the error:

Toplevel input, characters 9-15:
Error: Cannot find the elimination combinator ex_rec, the elimination of the
inductive definition ex on sort Set is probably not allowed

The problem is "Var" is an inductive definition of type "Type". Giving "Var"
type "Prop" solves the problem for me. Is there a way to get v without
turning Var's type to Prop?

Thank you all.

-----
Never say never.
-- 
View this message in context: 
http://www.nabble.com/Problem-with-rewriting-tp23853684p23910373.html
Sent from the Coq mailing list archive at Nabble.com.





Archive powered by MhonArc 2.6.16.

Top of Page