The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Hi Adam,

I'm already reading CPDT, this is how I learned about `return`s in
pattern matching and `refine` tactic and came up with a problem that
uses them. So I'm both reading and experimenting :-) .

---
Ömer Sinan Ağacan
http://osa1.net


2014-04-07 1:56 GMT+03:00 Adam Chlipala 
<adamc AT csail.mit.edu>:
> I'm sorry to be the "RTFM Parrot," but I think my answer to your last
> question is also the right one in this case: you should read an introduction
> to programming with dependent types in Coq, rather than trying to
> reconstruct the details through experimentation.
>
>
> On 04/06/2014 02:44 PM, Ömer Sinan Ağacan wrote:
>>
>> Let's say I have code like this:
>>
>>    refine (match n with
>>      | 0 =>  _
>>      | S n' =>  _
>>      end).
>>
>> In proof mode, I was expecting to get `n = 0` while filling first
>> underscore and `n = S n'` while filling second underscore, in fact I
>> can't make any progress in my program without this equalities. But Coq
>> doesn't give them to me as hypothesis. Why is this and what should I
>> do to have that equalities in proof mode?
>>