search

mietek / epigram2

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

PropSimp relies uses Higher Order terms #30

Closed GoogleCodeExporter closed 8 years ago

GoogleCodeExporter commented 8 years ago 
To get rid of Higher Order terms we're going to have to redesign 
Tactics.PropSimp. This doesn't look like a straight forward job.

Any takers?

Original issue reported on code.google.com by morris...@gmail.com on 21 Jun 2010 at 12:10

GoogleCodeExporter commented 8 years ago 
I am in the process of rewriting PropSimp so it produces terms rather than 
values, and the higher-order scopes will disappear.

Original comment by adamgundry on 12 Aug 2010 at 7:49

GoogleCodeExporter commented 8 years ago 
Done. The only use of HF left in the proposition simplifier can disappear as 
soon as the HF data constructor is removed. Now we just need to sort out 
telescopes to eradicate HF completely.

Original comment by adamgundry on 13 Aug 2010 at 10:06