mechvel

James writes > Ai! What can I have been thinking/doing!? > Apologies to all, I'd better have a long rethink. Today I fixed my Version 2 of proposal to the...

James writes " ``` IntegralDomain EuclideanDomain UniqueFactorisationDomain PrincipalIdealDomain ... ``` which is (probably) too big a project to identify as a single issue/PR? " My application has the first three....

jamesmckinna writes "As with #2542 and the subsequent proposal offered by @mechvel in #2559 , IIUC, it is possible to phrase 'no zero divisor' in a positive way. Where I...

Response to jamesmckinna : Symbolic computational (call it SC) mathematics is somewhat 1/4 of mathematics in the sense of the ideas and essential scientific content and value. Constructive mathematics is...

> Thanks @mechvel for the personal comments, but I think you're right: this isn''t the place, so my apologies for Alternatively you can write to me personally by email. The...

> Fixes https://github.com/agda/agda-stdlib/issues/2415 (I hope! @mechvel can you confirm that this reversion fixes > the problem with filter you raised there?). How can I check and confirm? Is this by...

> first, add my clone to your list of possible remote repositories > [..] I am sorry, this is too messy for me to arrange (I had an experience several...

> replace the rc1 version of src/Data/List/Base.agda with [this one](https://github.com/jamesmckinna/agda-stdlib > /blob/repair-v2.1-rc1/src/Data/List/Base.agda) > (the link is simply to the relevant file in the branch on GitHub defining the changes) >...

> Meanwhile @mechvel are you able to confirm that the 'old' behaviour wrt filter has been restored to your satisfaction? Yes, it is restored. I replaced the two .agda files...

> While I agree that we need to do this for 2.1, we also need to more deeply understand what's going on. The direct > implementation really ought to be...