G. Allais
G. Allais
Okay I think I have come around to this. Particularly because `quote` already has type: ``` quote : (0 _ : val) -> m TTImp ``` Once the merge conflict...
I tried to fix the evaluation issue we are getting in elab-util but could not find the issue. :/
Sorry, my wording was poor: I could not find a fix for the build issue.
Very interesting. The main code for the typechecking phase is in `processFailing` in `TTImp.ProcessDecls`. Could it be that a hole was delayed and we hit it in `checkDelayedHoles`? Should we...
I'm going to go ahead and tag this as good first issue because I assume it's something silly like overwriting the existing value with a record update instead of making...
If only we had a gadget that allowed us to express that something is the default without conflating it with the default value it takes. :thinking: http://gallais.github.io/blog/ceci-pas-default
Yeah I think it'd be nice to complain if there are conflicting declarations which means changing the merge strategy to take into account lack of value vs. value that happens...
> B = C B This is straight up an infinite loop.
This makes sense to me however it would be nice to know what the cause of the slowdown is. I don't think we're using many top level lazy constants in...
`+` is not injective. There is no hope to reconstruct unique `n1` and `n2` from `n1 + n2`.