Refactor constraints to syntactic form (Cstr)

[nilehmann]

No description provided.

[petros-marko]

LGTM 🚀

I see what you mean about Refinement.instNu... Could we avoid it if Cstr binders were not named?

[nilehmann]

I tried locally nameless, but that was worse because bound variables in types were being opened with free variables, so they had to be closed again to put them in the constraint. I think Refinement.instNu could be removed if we add an extra hypothesis to theorems requiring closed terms or if the vcgen ensured closed terms.

What I don't understand is why this didn't cause a problem before

[petros-marko]

I tried locally nameless, but that was worse because bound variables in types were being opened with free variables, so they had to be closed again to put them in the constraint. I think Refinement.instNu could be removed if we add an extra hypothesis to theorems requiring closed terms or if the vcgen ensured closed terms.

What I don't understand is why this didn't cause a problem before

I mean, since it's already written, is it worth to change it and add these hypotheses? even as is it's much closer to what's in the paper.

[nilehmann]

Can we merge this @petros-marko @jam-khan ?

[petros-marko]

Can we merge this @petros-marko @jam-khan ?

It's a yes from me 👍🏽

[jam-khan]

Can we merge this @petros-marko @jam-khan ?

Yes, looks good to me as well!