The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq users,

the term syntax table in the reference manual includes the following

        match_item ::= term [as name] [in pattern]

I came across some terms using this "match <term> in <pattern>" in proof 
goals, but I can't find the point in the reference manual, where the meaning 
of this is explained. A section reference in the term syntac table would be 
helpful.

As far as I understand from the cases I see, <pattern> is a pattern for the 
type of <term> and used to define identifiers for parts of the type term for 
use e.g. in a "result" term. Is this what it is, or is there more to know 
about this?

Best regards,

Michael