The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi Dimitri and James,

Thank you very much for your help! I'll have to spend some more time 
studying pattern matching. I also need to get over my aversion to using 
False_rect, which feels very discomfiting from a programming point of 
view, rather like:

    if (0 == 1) { ... perform complicated calculations that can never 
actually happen but must still type check ... }

Returning "I" dulls the pain somewhat :)

> Of course if you use this trick, then you still (might) need to do by 
> hand the equational pre-processing of families P which Epigram would do 
> for you in more complex examples such as Vec_tail, where you need to do 
> the equational reasoning to push a Vec n to a Vec m ... having 
> simplified Sm = Sn to m = n etc.

How usable is Epigram these days? I remember getting very excited about 
it back in 2005 I think it was, and looking forward to using it for 
development work. How the time goes.

> It is true that a true 'dependent pattern matching' vernacular syntax 
> would be very nice to have in Coq, ... so people have begun working on 
> this. In the meantime, let the optional 'return' clause in match 
> expressions be your friend...

Would that syntax actually be any different, or is it more a matter of 
getting Coq to do the rewriting by it self in the background, much as 
the Program mechanism purports to do?

Best regards,

Michael

--
Print XML with Prince!
http://www.princexml.com