Documentation

HexBasic.OfFn

source
def Hex.Array.ofFn' {α : Type u} {n : Nat} (f : Fin n → α) :
Array α

An Array.ofFn equivalent that reduces in the kernel under the module system.

Equations
Instances For
    source
    def Hex.Vector.ofFn' {n : Nat} {α : Type u} (f : Fin n → α) :
    Vector α n

    A Vector.ofFn equivalent that reduces in the kernel under the module system.

    Equations
    Instances For
      source
      @[simp]
      theorem Hex.Array.ofFn'_eq_ofFn {α : Type u} {n : Nat} (f : Fin n → α) :
      ofFn' f = Array.ofFn f
      source
      @[simp]
      theorem Hex.Vector.ofFn'_eq_ofFn {n : Nat} {α : Type u} (f : Fin n → α) :
      ofFn' f = Vector.ofFn f
      source
      @[simp]
      theorem Hex.Array.size_ofFn' {α : Type u} {n : Nat} (f : Fin n → α) :
      (ofFn' f).size = n
      source
      @[simp]
      theorem Hex.Array.getElem_ofFn' {α : Type u} {n : Nat} (f : Fin n → α) (i : Nat) (h : i < (ofFn' f).size) :
      (ofFn' f)[i] = f ⟨i, ⋯⟩
      source
      @[simp]
      theorem Hex.Vector.toArray_ofFn' {n : Nat} {α : Type u} (f : Fin n → α) :
      (ofFn' f).toArray = Array.ofFn' f
      source
      @[simp]
      theorem Hex.Vector.getElem_ofFn' {n : Nat} {α : Type u} (f : Fin n → α) (i : Nat) (h : i < n) :
      (ofFn' f)[i] = f ⟨i, h⟩
      source
      @[csimp]
      theorem Hex.Array.ofFn'_eq_ofFn' :
      @ofFn' = @Array.ofFn

      Compiled code uses the core Array.ofFn, which fills an array of known capacity instead of building a List first. The List route exists only so that the kernel can reduce it.

      source
      @[csimp]
      theorem Hex.Vector.ofFn'_eq_ofFn' :
      @ofFn' = @Vector.ofFn

      The Hex.Vector.ofFn' analogue of Hex.Array.ofFn'_eq_ofFn'.

      source
      def Hex.Array.map' {α : Type u} {β : Type v} (f : α → β) (a : Array α) :
      Array β

      An Array.map equivalent that reduces in the kernel under the module system: core Array.map's implementation loop is not exposed, so (a.map f) stalls downstream exactly like Array.ofFn. Remove this shim and migrate its callers to core Array.map when the pinned toolchain reaches Lean v4.35.0-rc1, which includes <https://github.com/leanprover/lean4/pull/14996>.

      Equations
      Instances For
        source
        @[simp]
        theorem Hex.Array.map'_eq_map {α : Type u} {β : Type v} (f : α → β) (a : Array α) :
        map' f a = Array.map f a
        source
        @[simp]
        theorem Hex.Array.size_map' {α : Type u} {β : Type v} (f : α → β) (a : Array α) :
        (map' f a).size = a.size
        source
        @[simp]
        theorem Hex.Array.getElem_map' {α : Type u} {β : Type v} (f : α → β) (a : Array α) (i : Nat) (h : i < (map' f a).size) :
        (map' f a)[i] = f a[i]
        source
        @[csimp]
        theorem Hex.Array.map'_eq_map' :
        @map' = @Array.map

        Compiled code uses the core Array.map, which writes into an array in place when uniquely referenced; the List route exists only so that the kernel can reduce it.

        source
        def Hex.Vector.map' {α : Type u} {β : Type v} {n : Nat} (f : α → β) (v : Vector α n) :
        Vector β n

        A Vector.map equivalent that reduces in the kernel under the module system: core Vector.map delegates to Array.map, whose implementation loop is not exposed, so (v.map f) stalls downstream. Remove this shim and migrate its callers to core Vector.map when the pinned toolchain reaches Lean v4.35.0-rc1, alongside Hex.Array.map'.

        Equations
        Instances For
          source
          @[simp]
          theorem Hex.Vector.map'_eq_map {α : Type u} {β : Type v} {n : Nat} (f : α → β) (v : Vector α n) :
          map' f v = Vector.map f v
          source
          @[simp]
          theorem Hex.Vector.toArray_map' {α : Type u} {β : Type v} {n : Nat} (f : α → β) (v : Vector α n) :
          (map' f v).toArray = Array.map' f v.toArray
          source
          @[simp]
          theorem Hex.Vector.getElem_map' {α : Type u} {β : Type v} {n : Nat} (f : α → β) (v : Vector α n) (i : Nat) (h : i < n) :
          (map' f v)[i] = f v[i]
          source
          @[csimp]
          theorem Hex.Vector.map'_eq_map' :
          @map' = @Vector.map

          Compiled code uses the core Vector.map; the List route exists only so that the kernel can reduce it.

          source
          def Hex.Array.zipWith' {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (a : Array α) (b : Array β) :
          Array γ

          An Array.zipWith equivalent that reduces in the kernel under the module system: core Array.zipWith runs its zipWithMAux loop by well-founded recursion, so (Array.zipWith f a b) stalls downstream exactly like Array.map. Remove this shim and migrate its callers to core Array.zipWith when the pinned toolchain reaches Lean v4.35.0-rc1, which includes <https://github.com/leanprover/lean4/pull/15078>.

          Equations
          Instances For
            source
            @[simp]
            theorem Hex.Array.zipWith'_eq_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (a : Array α) (b : Array β) :
            zipWith' f a b = Array.zipWith f a b
            source
            @[simp]
            theorem Hex.Array.size_zipWith' {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (a : Array α) (b : Array β) :
            (zipWith' f a b).size = min a.size b.size
            source
            @[simp]
            theorem Hex.Array.getElem_zipWith' {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (a : Array α) (b : Array β) (i : Nat) (h : i < (zipWith' f a b).size) :
            (zipWith' f a b)[i] = f a[i] b[i]
            source
            @[csimp]
            theorem Hex.Array.zipWith'_eq_zipWith' :
            @zipWith' = @Array.zipWith

            Compiled code uses the core Array.zipWith, which writes into an array of known capacity; the List route exists only so that the kernel can reduce it.