feat: Lean.RArray

[nomeata]

This PR adds the Lean.RArray data structure.

This data structure is equivalent to Fin n → α or Array α, but optimized for a fast kernel-reduction get operation.

It is not suitable as a general-purpose data structure. The primary intended use case is the “denote” function of a typical proof by reflection proof, where only the get operation is necessary, and where using List.get unnecessarily slows down proofs with more than a hand-full of atomic expressions.

There is no well-formedness invariant attached to this data structure, to keep it concise; it's semantics is given through RArray.get. In that way one can also view an RArray as a decision tree implementing Nat → α.

In #6068 this data structure is used in simp_arith.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6070 has successfully built against this PR. (2024-11-13 16:48:41) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e6e39f502feae04a0c40fc43ce2e259f74af3988 --onto 1315266dd3faeaf28d1263668cb88f2f3f5e530c. (2024-11-14 10:58:46)
• ✅ Mathlib branch lean-pr-testing-6070 has successfully built against this PR. (2024-11-14 11:11:04) View Log