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

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

Equations

• Lean.RArray.ofFn f h = Lean.RArray.ofFn.go f 0 n h ⋯

@[irreducible]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.RArray.ofArray xs h = Lean.RArray.ofFn (fun (x : Fin xs.size) => xs[x]) h

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

The correctness theorem for ofFn

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

@[simp]

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

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

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

Equations

• Lean.RArray.toExpr ty f (Lean.RArray.leaf x_1) = Lean.mkApp2 (Lean.mkConst `Lean.RArray.leaf) ty (f x_1)
• Lean.RArray.toExpr ty f (Lean.RArray.branch p l r) = Lean.mkApp4 (Lean.mkConst `Lean.RArray.branch) ty (Lean.mkRawNatLit p) (Lean.RArray.toExpr ty f l) (Lean.RArray.toExpr ty f r)

instance Lean.instToExprRArray {α : Type} [Lean.ToExpr α] : Lean.ToExpr (Lean.RArray α)

Equations

• Lean.instToExprRArray = { toExpr := fun (a : Lean.RArray α) => Lean.RArray.toExpr (Lean.toTypeExpr α) Lean.toExpr a, toTypeExpr := Lean.mkApp (Lean.mkConst `Lean.RArray) (Lean.toTypeExpr α) }