Defino así
Variable A:Set.
Inductive eq_list: list A -> list A -> Prop :=
eq_list0 : eq_list nil nil
| eq_listS : forall x y xl yl, eq x y -> eq_list xl yl -> eq_list (cons y yl)(cons x xl).
pero no me funciona con la definición de listas del teórico...me dice
Error:
In environment
A : Set
eq_list : list A -> list A -> Prop
The term "nil" has type "forall A : Set, list A"
while it is expected to have type "list A".
Hola.
No se qué versión estás usando, pero a mi me funciona:
Variable A:Set.
Inductive eq_list: list A -> list A -> Prop :=
eq_list0 : eq_list nil nil
| eq_listS : forall x y xl yl, eq x y -> eq_list xl yl -> eq_list (cons y yl)(cons x xl).
Probá en todo caso poniendo como primera línea:
Set Implicit Arguments.
El mensaje de error que te reporta es porque la lista está definida para elementos de un tipo genérico. Si ponés (nil A) en vez de nil el mensaje de error que te da sobre este constructor (que a mi no me aparece) desaparecería (lo mismo te va a pasar con Cons). Set Implicit Arguments (ver manual de Coq) se usa para que Coq infiera cierto tipos en las definiciones, evitando ponerlos en los usos de las definiciones.
Saludos, Carlos
