cmcmA20
cmcmA20
Let it chill until then, I will update it after release.
Can you also elaborate on interactions with `--cubical`, `--erased-cubical` and `--erased-matches`? I couldn't manage to reproduce #5910 with `--type-based-termination` + `--no-syntax-based-termination`.
``` go2 : Name → Term → TC ⊤ go2 cons-name hole = do raw-ty ← getType cons-name inf-ty ← inferType (con cons-name []) unify inf-ty raw-ty returnTC _ ```...
Btw, for a simplified example ``` data Copy (A : Set) : Set where mk-copy : A → Copy A ``` `checkExpr` reports a peculiar type ``` Checking {@0 A...
@andreasabel I guess it is. Slapping `workOnTypes` on top of all typechecker calls inside `tcReduce` resolves the problem with `go` but it feels ad hoc.
Yeah, feel free to suggest what other info should be exposed.
@JacquesCarette Sorry, I forgot about this PR! Jesper and Andreas have already merged these changes in #2432.
@andreasabel , is there anything else to take care of?
> The standard process for this is to _first_ make a new branch of the standard library compatible with this PR, then point this PR to that branch of the...
@jespercockx @andreasabel Thank you very much for finishing this PR and for shedding some light on the process of merging such changes!