-
Notifications
You must be signed in to change notification settings - Fork 12
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Idea: let Quote control unfolding #268
Comments
(Just as a remark, this is not as simple as it sounds -- we still need to be able to evaluate to a whnf, in order to implement the typechecker!! Conversion is not the only thing that matters.) |
If you allow the type checker to backtrack, that is, to raise |
What would be cool is if I could first evaluate without unfolding, and then tell the evaluator "OK, I want you to unfold this" etc., and just keep trying until things work. I think it might be plausible. |
(Then, the idea is that both the typechecker and the conversion checker/quotation would exploit this.) |
Maybe we shouldn't automatically unfold anything in evaluation, and instead rely on
Quote
to specifically request it during checking definitional equivalence. I think I see a way to make that work.The text was updated successfully, but these errors were encountered: