Documentation

Init.Data.Array.Set

@[extern lean_array_fset]
def Array.set {α : Type u_1} (xs : Array α) (i : Nat) (v : α) (h : i < xs.size := by get_elem_tactic) :

Replaces the element at a given index in an array.

No bounds check is performed, but the function requires a proof that the index is in bounds. This proof can usually be omitted, and will be synthesized automatically.

The array is modified in-place if there are no other references to it.

Examples:

  • #[0, 1, 2].set 1 5 = #[0, 5, 2]
  • #["orange", "apple"].set 1 "grape" = #["orange", "grape"]
Equations
    Instances For
      @[inline]
      def Array.setIfInBounds {α : Type u_1} (xs : Array α) (i : Nat) (v : α) :

      Replaces the element at the provided index in an array. The array is returned unmodified if the index is out of bounds.

      The array is modified in-place if there are no other references to it.

      Examples:

      Equations
        Instances For
          @[extern lean_array_set]
          def Array.set! {α : Type u_1} (xs : Array α) (i : Nat) (v : α) :

          Set an element in an array, or panic if the index is out of bounds.

          This will perform the update destructively provided that a has a reference count of 1 when called.

          Equations
            Instances For