The Coq mailing list

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

Dear Adam,

thanks for the pointer! Section 8.1 "Length-Indexed Lists" explains the "in 
clause" very well. I guess it is time for me to read your book.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Adam Chlipala
Sent: Monday, February 09, 2015 2:47 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] What does Galina "match <term> in <pattern>" mean?

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