The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hi,
The x inside the return is actually bound by the "as x" occurring just before.

Indeed (eq_refl optA) is the proof of optA=optA. but the return clause
does not specify the type of the match, it specifies the type "scheme"
of each of its branches. The type of the match is computed by applying
the scheme to the matched term (ie optA), which gives ((fun x=> optA=x
=> nat) optA) i.e. optA=optA -> nat.

Indeed if you remove the refl_equal:

Variable A:Set.
Definition f (optA : option A) :=
(match optA as x return optA = x -> nat with
 | Some a => (fun p => O)
 | None => (fun p => 1)
end).

Check f.

you obtain that f is of type optA=optA -> nat.

Hope this helps,
Pierre

2011/7/13 Marco Servetto 
<marco.servetto AT gmail.com>:
> Hi, thank you, the return "trik" works with minor twiking.
> However it really leave me in the total misunderstanding of why it works:
>
> I was thinking (eq_refl optA) to produce a proof for optA=optA, not
> for optA=x, moreover x looks out of
> scope outside the parenthesis of the match... may be I have to study
> what exactly the return does.
>
>> Definition f (optA : option A) :=
>> (match optA as x return optA = x -> nat with
>>  | Some a => (fun p => O)
>>  | None => (fun p => 1)
>> end) (eq_refl optA).
>
> And again,  thank you all!
> Marco.
>
>