Yury G. Kudryashov comments

Results 116 comments of


                                            Yury G. Kudryashov

feat: add `Decidable` linter

@grunweg Linter flags `GeneralizeProofs` now. I can't find the relevant @kmill's comment. Was it here or on Zulip?

feat: add `Decidable` linter

Is there a way to test for a function being partial? If yes, then we should do it.

feat: add `Decidable` linter

!bench

feat: add `Decidable` linter

Should we merge it now?

feat: add `Decidable` linter

!bench

Merge 3 files about basic properties of relations

@robertylewis #1562 was too large and had some loosely related parts, so I closed it without merging. I'll try to revive some parts of it next week.

feat: prove Cauchy's upper bound on polynomial roots

I'm going to move lemmas from `Nonneg` tonight.

feat: prove Cauchy's upper bound on polynomial roots

Thanks! bors d+

chore (Algebra.Order.Nonneg.Ring): split into unbundled and bundled ordered algebra files

bors failed, probably because of this file. Removing from the queue, delegating, and merging `master`. bors r- bors d+

module: add `:lang lean4`

At the moment, `lean4-mode` only works with `lsp-mode`. There are plans to make it work with `eglot` in the future, but it's not there yet. About lean3: there are still...