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

Equations

• a.get n = Lean.RArray.rec (fun (x : α) => x) (fun (p : Nat) (x x : Lean.RArray α) (l r : α) => Bool.rec l r (p.ble n)) a

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

RArray.get, implemented conventionally

Equations

• (Lean.RArray.leaf x).getImpl n = x
• (Lean.RArray.branch p l r).getImpl n = if n < p then l.getImpl n else r.getImpl n

@[csimp]

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

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

Equations

• Lean.instGetElemRArrayNatTrue = { getElem := fun (a : Lean.RArray α) (n : Nat) (x : True) => a.get n }

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

Equations

• (Lean.RArray.leaf x).size = 1
• (Lean.RArray.branch p l r).size = l.size + r.size