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

Distinguish lazy and eager elaboration #76

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
When Elab needs to solve a subproblem, it should be able to indicate whether it 
should be solved eagerly (i.e. with as much local progress as possible before 
the calling process continues) or lazily (i.e. left as a metavariable with a 
suspended problem). To handle applications, it should eagerly elaborate the 
head, insist its type is canonical, then lazily elaborate the arguments. The 
scheduler also needs to be modified to solve constraints before elaborating 
display syntax, thereby providing the maximum amount of information to 
elaboration.

Original issue reported on code.google.com by adamgundry on 3 Sep 2010 at 3:01