search

mwleeds / epigram

Automatically exported from code.google.com/p/epigram
0 stars 0 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