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

ProofState.Interface.Lifting is not an Interface #44

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
At first glance, this file is not an Interface but a bit of Structure. It might 
well be merged to ProofState.Structure.Scope.

Original issue reported on code.google.com by pedag...@gmail.com on 11 Aug 2010 at 7:43

GoogleCodeExporter commented 9 years ago 
Oh, and it needs a clean-up. 

Also, PropSimp being rewritten to work on Terms instead of Values, chances are 
that most of this becomes dead code. In which case, please garbage collect.

Original comment by pedag...@gmail.com on 11 Aug 2010 at 9:55

GoogleCodeExporter commented 9 years ago 
I am rewriting Lifting in the course of tidying up PropSimp, since it is used 
fairly heavily there and almost nowhere else. I will try to find an appropriate 
place to put the rewritten version.

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

GoogleCodeExporter commented 9 years ago 
Much of the rewritten code from Lifting has now moved to Evidences.Utilities. I 
am not sure where the remainder should go, any thoughts?

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