mechvel

I recall the story. Initially it was ``` _∣_ : Rel A _ x ∣ y = ∃ \ q → q ∙ x ≈ y ``` (transpositions possible). It...

> I'm sorry to hear that the v2.0 changes are still causing you problems a) I thought that ``∃ \ q → q ∙ x ≈ y`` was the best...

> a) this issue seems intractable unless we can agree sensible measures against which to judge 'best'. At the moment there > is simply an impasse between conflicting views. About...

I am trying to understand what promises your phrase > and v3.0 as the opportunity to clean up a lot of suboptimal legacy design > decisions, many of which have...

I wrote > How it was in lib-1.7.1 it can be seen in > http://www.botik.ru/pub/local/Mechveliani/inAgda/admissiblePPO-wellFounded.zip As you are going to look into this source, your comments are welcome in general.

I do not believe that the above two possible changes have sense. And even if they do, they do not worth the dispenses they would cause for users.

I keep on asking the team to return to the definition ``` ∃ \ q → q ∙ x ≈ y ``` For example, I have in the name space...

The feature is crucial for programmers. For example, a program must not confuse of what is happening in the domain of the module OfVector(n) and in the domain of the...

For any occasion, I copy here my bug report from Zulip. This is on Agda version 2.7.0.1 Built with flags (cabal -f) - optimise-heavily: extra optimisations, ghc-9.0.2, stdlib-2.1.1 Type checking:...

Thank you for explanation. Now, when it is given ``(S : Setoid a ℓ)``, is there a way to apply the above ``(composeSetoid n S)`` ? To help this, I...