Buenas,
He notado que al hacer un pattern matching en un tipo instanciado a partir de un tipo paramétrico le tengo que seguir pasando el tipo que ya instancie.
Ej:
Inductive list (A:Set) : Set :=
nil : list A
| cons : A -> list A -> list A.
Definition listN := list nat.
Fixpoint member (n:nat)(l:listN) :=
match l with
nil _ => false (Si no le paso el wildcard me tira un error!!)
....
¿Porque le tengo que seguir pasando el wildcard a nil si ese wildcard se corresponde con nat que fue instanciado en la definición de listN?
¿No debería funcionar como si hubiera hecho una beta-reducción de aplicar el tipo a la funcion?
Saludos.