Conversation
| -- annotate with a hole): @{? λx.x : ? ?}@. The other possible choice | ||
| -- is to require the wrapped expression to be checkable against the | ||
| -- hole type: this is mildly more permissive since a bare lambda is |
There was a problem hiding this comment.
I actually think that changing to this other approach may be better.
There was a problem hiding this comment.
I actually think that changing to this other approach may be better.
I'm a bit confused by this comment: nothing is changing here, is it? We're just documenting the current behavior?
There was a problem hiding this comment.
Does this mean you're proposing we stick with the current implementation, rather than #931?
There was a problem hiding this comment.
Nothing is changing in this PR, just documenting the current behaviour.
I still think we should move ahead with #931.
There was a problem hiding this comment.
Ahh, ok, thanks for clarifying. I had worried that this PR meant you'd changed your mind on #931.
brprice
force-pushed
the
brprice/doc-hole-bidir
branch
from
deed325 to
b38a3d9
Compare
|
Are these old issues related, and do they need revisiting? |
I don't think this is particularly related -- it talks about viewing holes from the outside, and the current pr is about viewing from the inside.
This is related because if we prevent this, then writing
This seems fairly unrelated to me. In general it would be nice to revisit all those issues, but I don't currently have any good ideas about them. (One half-baked idea is to do more inference / record constraints -- then at least we would be able to tell the student when a hole annotation is unfillable) |
3 participants
No description provided.