coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Problem with rewriting, dimitrisg7
- Re: [Coq-Club] Problem with rewriting, Edsko de Vries
- Re: [Coq-Club] Problem with rewriting, Adam Chlipala
- Re: [Coq-Club] Problem with rewriting,
muad
- Re: [Coq-Club] Problem with rewriting,
Pierre Casteran
- Re: [Coq-Club] Problem with rewriting, dimitrisg7
- Re: [Coq-Club] Problem with rewriting,
Pierre Casteran
- Re: [Coq-Club] Problem with rewriting, dimitrisg7
- Re: [Coq-Club] Problem with rewriting, Adam Chlipala
Archive powered by MhonArc 2.6.16.