The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

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.