Documentation

Lean.Data.RArray

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) :
Equations
    Instances For
      @[irreducible]
      def Lean.RArray.ofFn.go {α : Type u_1} {n : Nat} (f : Fin nα) (lb ub : Nat) (h1 : lb < ub) (h2 : ub n) :
      Equations
        Instances For
          def Lean.RArray.ofArray {α : Type u_1} (xs : Array α) (h : 0 < xs.size) :
          Equations
            Instances For
              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 α) :
              Equations
                Instances For
                  def Lean.RArray.toExpr.go {α : Type u_1} (ty : Expr) (f : αExpr) (leaf branch : Expr) (a : RArray α) :
                  Equations
                    Instances For