source
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 α

Instances For

source
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_1 : Lean.RArray α) (l r : α) => Bool.rec l r (p.ble n)) a

Instances For

source
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

Instances For

source
@[csimp]
theorem Lean.RArray.get_eq_getImpl :
@get = @getImpl
source
instance Lean.instGetElemRArrayNatTrue {α : Type u} :
GetElem (RArray α) Nat α fun (x : RArray α) (x_1 : Nat) => True
Equations

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

source
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

Instances For