Joe Hendrix
Joe Hendrix
### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues). *...
This replaces a few uses of initialize with builtin_initialize, and removes some unneeded functionality added when it was unclear if lazy discriminator trees would be efficient enough.
This is still a work in progress.
This uses the associativity, commutativity and identity classes recently added to Lean core to define folds with simplification lemmas that can move intermediate results outside the fold for better use...
Lean should provide `Int8`, `Int16`, `Int32` and `Int64` to complement `UInt8`, `UInt16`, `UInt32`, and `UInt64`. Ideally the definitions should be in core and the compiler extended to generate efficient code...
This is a draft document that describes desired features in the standard library. I thought I'd submit it as a PR to the repo itself for now for feedback, but...
As part of helping new users, we should codify naming conventions for theorems in the standard library. Related discussions: * See [this comment](https://github.com/leanprover/std4/pull/329#issuecomment-1786193983) in #329.
This repo is upstream from Mathlib, but we'd like to ensure changes to `main` do not break Mathlib. Should we add a build step or task that builds Mathlib (perhaps...