The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Vincent BENAYOUN wrote:
> Does anyone can explain me the signification of the error I get with 
> the below example ?
>
> Error message : *The term "v" has type "nat" while it is expected to 
> have type
>  "Datatypes.nat".*
>
> Definition records_convert (r : my_records) :=
>   match r with
>     | My_Record nat _ "a" v My_EmptyRecord => Record1 v
>     | My_Record string _ "b" b (My_Record nat _ "c" c My_EmptyRecord) 
> => Record2 b c
>     | _ => Match0_other (* I need to be exhaustive *)
>   end.

You are using [nat] as a pattern variable, so it is bound locally in the 
first pattern to whatever type appears as the first argument to 
[My_Record].  It is impossible to pattern-match on types, so you will 
need to introduce an extra level of syntax and interpretation if you 
want to write this kind of code.