inductive Lean.RArray (α : Type u) : Type u

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.

• leaf {α : Type u} : α → RArray α
• branch {α : Type u} : Nat → RArray α → RArray α → RArray α

noncomputable def Lean.RArray.get {α : Type u} (a : RArray α) (n : Nat) : α

The crucial operation, written with very little abstractional overhead

def Lean.RArray.getImpl {α : Type u} (a : RArray α) (n : Nat) : α

RArray.get, implemented conventionally

@[csimp]

theorem Lean.RArray.get_eq_getImpl : @get = @getImpl

instance Lean.instGetElemRArrayNatTrue {α : Type u} : GetElem (RArray α) Nat α fun (x : RArray α) (x : Nat) => True

def Lean.RArray.size {α : Type u} : RArray α → Nat