Zulip Chat Archive

The decidable_classical Linter is quite unhappy about src/ring_theory/polynomial/homogenization.lean... I've added some @[nolint decidable_classical] to keep the green sign on GitHub, but sooner or later we will have to fix these.

Alex J. Best (Nov 22 2021 at 14:57):

Yeah I don't know how to fix them unfortunately

Alex J. Best (Nov 22 2021 at 14:57):

Adding nolint make sense in that case though, thanks

Riccardo Brasca (Nov 22 2021 at 15:30):

It's fixed now, without all the nolint.

Riccardo Brasca (Nov 22 2021 at 15:30):

I am not sure it is the best way of doing this, but you can see all the change in commit c813f0f.

Alex J. Best (Nov 22 2021 at 15:42):

Oh nice thanks, yeah that looks good, tbh I didn't realise I still had open locale classical in the file

David Ang (Nov 08 2022 at 20:11):

Hello, are there any plans to PR large chunks of this file into mathlib (or should the “correct” definition of homogenisation in mathlib be more general?)? I’m not part of this project, but I need this for something else, and I’m happy to help out with the golfing or documentation etc if necessary!

Riccardo Brasca (Nov 08 2022 at 20:19):

cc @Alex J. Best that I think wrote it

Alex J. Best (Nov 08 2022 at 22:55):

There are plans in my head to PR it but i don't have a lot of time for that right now (but I'd like to do so within a month let's say), i think the definitions are good and don't necessarily need changing for mathlib. Do you need it for something you are PRing to mathlib very soon? Feel free to use it of course, and to make contributions!