chore: avoid runtime array bounds checks (#6134) This PR avoids runtime array bounds checks in places where it can trivially be done at compile time. None of these changes are of particular consequence: I mostly wanted to learn how much we do this, and what the obstacles are to doing it less.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).