A RArray
can model Fin n → α
or Array α
, but is optimized for a fast kernel-reducible get
operation.
The primary intended use case is the “denote” function of a typical proof by reflection proof, where
only the get
operation is necessary. It is not suitable as a general-purpose data structure.
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 → α
.
See RArray.ofFn
and RArray.ofArray
in module Lean.Data.RArray
for functions that construct an
RArray
.
Instances For
The crucial operation, written with very little abstractional overhead