leanprover-bot

icon location Might do useful things on Lean repos maintainer: @Kha

Results 202 comments of leanprover-bot

perf: parallelize `rw?` tactic

Reference manual CI status: - ❗ Reference manual CI will not be attempted unless your PR branches off the `nightly-with-manual` branch. Try `git rebase e1f8c147e72504b88f7275005df32e892e19a08b --onto d3dda9f6d4428a906c096067ecb75e432afc4615`. You can force...

perf: better Char.toLower/Char.toUpper implementation

Reference manual CI status: - ❗ Reference manual CI can not be attempted yet, as the `nightly-testing-2025-12-16` tag does not exist there yet. We will retry when you push more...

feat: allow numeric literals to be coerced to option type

Reference manual CI status: - ❗ Reference manual CI will not be attempted unless your PR branches off the `nightly-with-manual` branch. Try `git rebase 6d5efd79b9d751a487c4b3049e283fc412b0179e --onto d3dda9f6d4428a906c096067ecb75e432afc4615`. You can force...

refactor: grind AIG proofs into dust

Reference manual CI status: - ❗ Reference manual CI will not be attempted unless your PR branches off the `nightly-with-manual` branch. Try `git rebase 6469890178986678af97999948b0dd7173554af2 --onto eee58f4506d28a14c9a171165f999445a0663d93`. You can force...

chore: fmt bench

Reference manual CI status: - ❗ Reference manual CI will not be attempted unless your PR branches off the `nightly-with-manual` branch. Try `git rebase c41cb64ca7cd86a0519d009532bad87bc87e9d2a --onto d3dda9f6d4428a906c096067ecb75e432afc4615`. You can force...

refactor: move Std.Range to Std.Legacy.Range

Reference manual CI status: - ❗ Reference manual CI can not be attempted yet, as the `nightly-testing-2025-12-01` tag does not exist there yet. We will retry when you push more...

feat: proper recursive specialization

Reference manual CI status: - ❗ Reference manual CI will not be attempted unless your PR branches off the `nightly-with-manual` branch. Try `git rebase edcef51434804e6432c02f42ef364cb13f9149b2 --onto d3dda9f6d4428a906c096067ecb75e432afc4615`. You can force...

chore: make `Subrelation` reducible

Reference manual CI status: - ❗ Reference manual CI will not be attempted unless your PR branches off the `nightly-with-manual` branch. Try `git rebase 38b4062edb5f14185df19d702953756f48ceaba0 --onto d3dda9f6d4428a906c096067ecb75e432afc4615`. You can force...

doc: adds missing docstrings related to iterators and ranges

Reference manual CI status: - ❗ Reference manual CI will not be attempted unless your PR branches off the `nightly-with-manual` branch. Try `git rebase bf51e1dcfa3322f639cb17e283a9b8caa1c16209 --onto 62f2f9229356039356c0469a46d8ecd77be88e2a`. You can force...

fix: do not modify infotrees in `withSetOptionIn`

Reference manual CI status: - ❗ Reference manual CI can not be attempted yet, as the `nightly-testing-2025-11-21` tag does not exist there yet. We will retry when you push more...