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

Extracting the Elaborator DSL from the Elaborator for DisplayLang #43

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
Currently, the Elaborator DSL (ElabMonad and friends) is presented with the 
Elaborator from Display terms to Evidences. 

However, in spirit, the Elaborator DSL is more general than that: it ought to 
work as well to write an elaborator for an high-level syntax (a la Epigram 1 
for instance) down to whatever you want.

So, to make this clear, we should extract (and, if necessary, decouple) the 
definition of the ElabMonad from its use for the DisplayLang.

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