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

Elimination w/ motive: the parametric/non-parametric oracle is bogus #81

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
For a reason we have not yet understood (when not giving the "comma" term in 
elimination with a motive), the parametric/non-parametric detection code is 
bogus. It will compute things as non-parametric while they obviously are, based 
on their position in the goal.

We suspect something like "lambda-lifting gone wrong", but lack formal 
evidences and don't really understand what this code is doing.

(I will push a test case and advertise it here later on)

Original issue reported on code.google.com by pedag...@gmail.com on 5 Sep 2010 at 11:29

GoogleCodeExporter commented 9 years ago 
Actually, I mis-understood what should be parameterised, what should not. The 
results were correct. Three cheers for Elimination with a Motive!

Original comment by pedag...@gmail.com on 6 Sep 2010 at 2:07