13.2 About patterns of parametric types
When matching objects of a parametric type, constructors in patterns do not expect the parameter arguments. Their value is deduced during expansion.Consider for example the polymorphic lists:
Coq < Inductive List [A:Set] :Set := Coq < nil:(List A) Coq < | cons:A->(List A)->(List A).List_ind is defined
List_rec is defined
List_rect is defined
List is defined
We can check the function tail:
Coq < Check [l:(List nat)]Cases l of Coq < nil => (nil nat)Coq < | (cons _ l') => l'Coq < end.[l:(List nat)]Cases l of
nil => (nil nat)
| (cons _ l') => l'
end
: (List nat)->(List nat)
When we use parameters in patterns there is an error message:
Coq < Check [l:(List nat)]Cases l of Coq < (nil nat) => (nil nat)Coq < | (cons nat _ l') => l'Coq < end.Toplevel input, characters 6-169
> ..... [l:(List nat)]Cases l of
> (nil nat) => (nil nat)
> | (cons nat _ l') => l'
> end
Error: The term
[l:(List nat)]
Cases l of
(nil dum_nat) => (nil dum_nat)
| (cons dum_nat dum__ dum_l') => dum_l'
end failed to typecheck:
In pattern (nil nat) the constructor nil expects 0 arguments.