Nils Anders Danielsson comments

Results 325 comments of


                                            Nils Anders Danielsson

Solving blocked terms loses the user-written code

Bisection points to 47358b362129b6848ec9d6ea57c626e321ffb261 ("[ #3435 ] postpone instance constraints while checking applications").

Solving blocked terms loses the user-written code

That file is easy to fix, just replace ```agda cong (_ ,_) (trans (sym $ subst-refl _ _) (subst-refl _ _)) ≡⟨ cong (cong _) (trans-symˡ _) ⟩ ``` with...

Solving blocked terms loses the user-written code

An aside: If I turn on `--no-syntactic-equality`, then there are unsolved constraints in many type signatures in that file. The option is described as a shortcut, and I thought that...

Solving blocked terms loses the user-written code

I opened a new ticket for the issue with `--no-syntactic-equality` (#4265).

Solving blocked terms loses the user-written code

Is it time to go ahead with this change now? Here is another test case: ```agda {-# OPTIONS --cubical #-} open import Agda.Builtin.Cubical.Path postulate trans : {A : Set} {x...

Solving blocked terms loses the user-written code

I'm trying to merge the master branch into the issue4067 branch.

Solving blocked terms loses the user-written code

@vlopezj, how would Tog handle this situation?

Solving blocked terms loses the user-written code

I'm not convinced that it makes sense to fix this issue by making constraint solving less robust. However, I do think it makes sense to preserve user-written code. Is it...

Solving blocked terms loses the user-written code

> I'm trying to merge the master branch into the issue4067 branch. Done.

Solving blocked terms loses the user-written code

I saw that `cubical-test` fails for the `issue4067` branch. (I failed to notice this before pushing because the test was not set up properly, but I have fixed that on...