This module provides slice notation for array slices (a.k.a. Subarray) and implements an iterator for those slices.

instance instSliceableArrayNatSubarray {α : Type u} : Std.Rcc.Sliceable (Array α) Nat (Subarray α)

Equations

• instSliceableArrayNatSubarray = { mkSlice := fun (xs : Array α) (range : Std.Rcc Nat) => xs.toSubarray range.lower (range.upper + 1) }

instance instSliceableArrayNatSubarray_1 {α : Type u} : Std.Rco.Sliceable (Array α) Nat (Subarray α)

Equations

• instSliceableArrayNatSubarray_1 = { mkSlice := fun (xs : Array α) (range : Std.Rco Nat) => xs.toSubarray range.lower range.upper }

instance instSliceableArrayNatSubarray_2 {α : Type u} : Std.Rci.Sliceable (Array α) Nat (Subarray α)

Equations

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

instance instSliceableArrayNatSubarray_3 {α : Type u} : Std.Roc.Sliceable (Array α) Nat (Subarray α)

Equations

• instSliceableArrayNatSubarray_3 = { mkSlice := fun (xs : Array α) (range : Std.Roc Nat) => xs.toSubarray (range.lower + 1) (range.upper + 1) }

instance instSliceableArrayNatSubarray_4 {α : Type u} : Std.Roo.Sliceable (Array α) Nat (Subarray α)

Equations

• instSliceableArrayNatSubarray_4 = { mkSlice := fun (xs : Array α) (range : Std.Roo Nat) => xs.toSubarray (range.lower + 1) range.upper }

instance instSliceableArrayNatSubarray_5 {α : Type u} : Std.Roi.Sliceable (Array α) Nat (Subarray α)

Equations

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

instance instSliceableArrayNatSubarray_6 {α : Type u} : Std.Ric.Sliceable (Array α) Nat (Subarray α)

Equations

• instSliceableArrayNatSubarray_6 = { mkSlice := fun (xs : Array α) (range : Std.Ric Nat) => xs.toSubarray 0 (range.upper + 1) }

instance instSliceableArrayNatSubarray_7 {α : Type u} : Std.Rio.Sliceable (Array α) Nat (Subarray α)

Equations

• instSliceableArrayNatSubarray_7 = { mkSlice := fun (xs : Array α) (range : Std.Rio Nat) => xs.toSubarray 0 range.upper }

instance instSliceableArrayNatSubarray_8 {α : Type u} : Std.Rii.Sliceable (Array α) Nat (Subarray α)

Equations

• instSliceableArrayNatSubarray_8 = { mkSlice := fun (xs : Array α) (x : Std.Rii Nat) => xs.toSubarray }

instance instSliceableSubarrayNat {α : Type u} : Std.Rcc.Sliceable (Subarray α) Nat (Subarray α)

Equations

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

instance instSliceableSubarrayNat_1 {α : Type u} : Std.Rco.Sliceable (Subarray α) Nat (Subarray α)

Equations

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

instance instSliceableSubarrayNat_2 {α : Type u} : Std.Rci.Sliceable (Subarray α) Nat (Subarray α)

Equations

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

instance instSliceableSubarrayNat_3 {α : Type u} : Std.Roc.Sliceable (Subarray α) Nat (Subarray α)

Equations

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

instance instSliceableSubarrayNat_4 {α : Type u} : Std.Roo.Sliceable (Subarray α) Nat (Subarray α)

Equations

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

instance instSliceableSubarrayNat_5 {α : Type u} : Std.Roi.Sliceable (Subarray α) Nat (Subarray α)

Equations

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

instance instSliceableSubarrayNat_6 {α : Type u} : Std.Ric.Sliceable (Subarray α) Nat (Subarray α)

Equations

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

instance instSliceableSubarrayNat_7 {α : Type u} : Std.Rio.Sliceable (Subarray α) Nat (Subarray α)

Equations

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

instance instSliceableSubarrayNat_8 {α : Type u} : Std.Rii.Sliceable (Subarray α) Nat (Subarray α)

Equations

• instSliceableSubarrayNat_8 = { mkSlice := fun (xs : Subarray α) (x : Std.Rii Nat) => xs }