Olle Fredriksson
Olle Fredriksson
I'm not too familiar with Tape, but I see that there's a `tape-promise` library. Could that work?
Any ideas for doing it without duplicating the whole of `search`?
Nice, thanks for looking into it! I'll try it out and report back to you when I get the chance to do so.
Fixes https://github.com/danr/proptest/issues/11
There are some experiments happening over at https://github.com/ollef/sixty. Cheers @brendanzab! I'll probably bug you for help when I get stuck.
It depends on how the experiment goes. I'm a bit worried that the "no substitution" trick will break down when you get to pattern matching elaboration, because you then need...
Your approach seems to solve the index shifting problem, but don't the values still have levels that need to be shifted (in the other direction) as well? I wonder if...
I could be wrong, but I think it's still an issue: If we're adding bindings in the middle of the context, the values that are already in the context will...
When elaborating `case x of Con y z -> rhs`, you replace `x` in the context with `y, z`. Or, like I do in Sixten to avoid removing entries, put...
Hmm, I think I need your solution spelled out to understand it. What we need for dependent matching is that when typechecking `rhs` in `case x of Con y z...