Auxiliary definitions related to Lean.RArray that are typically only used in meta-code, in particular the ToExpr instance.

def Lean.RArray.ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) (h : 0 < n) : RArray α

@[irreducible]

def Lean.RArray.ofFn.go {α : Type u_1} {n : Nat} (f : Fin n → α) (lb ub : Nat) (h1 : lb < ub) (h2 : ub ≤ n) : RArray α

def Lean.RArray.ofArray {α : Type u_1} (xs : Array α) (h : 0 < xs.size) : RArray α

theorem Lean.RArray.get_ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) (h : 0 < n) (i : Fin n) : (ofFn f h).get ↑i = f i

The correctness theorem for ofFn

theorem Lean.RArray.get_ofFn.go {α : Type u_1} {n : Nat} (f : Fin n → α) (i : Fin n) (lb ub : Nat) (h1 : lb < ub) (h2 : ub ≤ n) (h3 : lb ≤ ↑i) : ↑i < ub → (ofFn.go f lb ub h1 h2).get ↑i = f i

@[simp]

theorem Lean.RArray.size_ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) (h : 0 < n) : (ofFn f h).size = n

theorem Lean.RArray.size_ofFn.go {α : Type u_1} {n : Nat} (f : Fin n → α) (lb ub : Nat) (h1 : lb < ub) (h2 : ub ≤ n) : (ofFn.go f lb ub h1 h2).size = ub - lb

def Lean.RArray.toExpr {α : Type u_1} (ty : Expr) (f : α → Expr) (a : RArray α) : MetaM Expr

def Lean.RArray.toExpr.go {α : Type u_1} (ty : Expr) (f : α → Expr) (leaf branch : Expr) (a : RArray α) : MetaM Expr