The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Part II of CPDT <http://adam.chlipala.net/cpdt/> introduces this idea.  
It doesn't correspond to anything from more conventional functional 
programming.

On 02/09/2015 08:36 AM, Soegtrop, Michael wrote:
> 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