hazelgrove/agda-popl17

constructability

Closed this issue · 2 comments

ivoysey commented
  • refactor proof to the form that doesn't use the needless judgements, so you can stick whatever you want in the lists whenever you want to
  • define a finish normal form and see if that lets you avoid needing to construct filled holes? but that would break the subsume hack, since we specifically envelop the term to protect it from analysis.
cyrus- commented

The finish normal firm business should probably be it's own issue?

ivoysey commented

yeah, that's a good call.