Buenas, nos está pasando con mi compañera que para el mismo código si yo agrego un underscore en el lugar del tipo en una definición que usa match a mí me funciona mientras que a ella Coq le dice "Error: The constructor X expects no arguments". Por otro lado, si ella omite el underscore le funciona bien, mientras que a mí me da error "The constructor X is expected to be applied to 1 argument while it is actually applied to no arguments".
Ejemplo:
Como me funciona a mí:
Definition is_nil (A:Set) (l : list A) :=
match l with
| nil _ => true
| cons _ _ l => false
end.
Como le funciona a mi compañera:
Definition is_nil (A:Set) (l : list A) :=
match l with
| nil => true
| cons _ l => false
end.
Puede ser que sean versiones distintas de Coq? Se puede entregar cualquiera de las dos formas?
Gracias de antemano, saludos.