search

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
48 stars 7 forks source link

Matching code is broken #113

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
The code in Tactics.Matching assumes all eliminators are injective, and does 
not check that its solutions for references are type-correct. This means it can 
give invalid solutions in obscure circumstances. We need better higher-order 
matching, but in the meantime it might be enough to check type-correctness and 
give a sound but incomplete matching procedure.

Original issue reported on code.google.com by adamgundry on 29 Sep 2010 at 6:55