Init.Data.Slice.Array.Basic

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

source

@[instance_reducible]

instance instSliceableArrayNatSubarray {α : Type u} :

Std.Rcc.Sliceable (Array α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableArrayNatSubarray_1 {α : Type u} :

Std.Rco.Sliceable (Array α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableArrayNatSubarray_2 {α : Type u} :

Std.Rci.Sliceable (Array α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableArrayNatSubarray_3 {α : Type u} :

Std.Roc.Sliceable (Array α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableArrayNatSubarray_4 {α : Type u} :

Std.Roo.Sliceable (Array α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableArrayNatSubarray_5 {α : Type u} :

Std.Roi.Sliceable (Array α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableArrayNatSubarray_6 {α : Type u} :

Std.Ric.Sliceable (Array α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableArrayNatSubarray_7 {α : Type u} :

Std.Rio.Sliceable (Array α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableArrayNatSubarray_8 {α : Type u} :

Std.Rii.Sliceable (Array α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableSubarrayNat {α : Type u} :

Std.Rcc.Sliceable (Subarray α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableSubarrayNat_1 {α : Type u} :

Std.Rco.Sliceable (Subarray α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableSubarrayNat_2 {α : Type u} :

Std.Rci.Sliceable (Subarray α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableSubarrayNat_3 {α : Type u} :

Std.Roc.Sliceable (Subarray α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableSubarrayNat_4 {α : Type u} :

Std.Roo.Sliceable (Subarray α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableSubarrayNat_5 {α : Type u} :

Std.Roi.Sliceable (Subarray α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableSubarrayNat_6 {α : Type u} :

Std.Ric.Sliceable (Subarray α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableSubarrayNat_7 {α : Type u} :

Std.Rio.Sliceable (Subarray α) Nat (Subarray α)

source

@[instance_reducible]

instance instSliceableSubarrayNat_8 {α : Type u} :

Std.Rii.Sliceable (Subarray α) Nat (Subarray α)