inductive Lean.RArray (α : Type) : Type

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.

It is not universe-polymorphic. ; smaller proof objects and no complication with the ToExpr type class.

• leaf {α : Type} : α → Lean.RArray α
• branch {α : Type} : Nat → Lean.RArray α → Lean.RArray α → Lean.RArray α

noncomputable def Lean.RArray.get {α : Type} (a : Lean.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} (a : Lean.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 : @Lean.RArray.get = @Lean.RArray.getImpl

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

Equations

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

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

Equations

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