class Data.Ix (α : Type u) : Type u

Typeclass for indexable types supporting range enumeration.

$$\text{Ix}(\alpha)$$ provides operations for enumerating and indexing over bounded ranges $[lo, hi]$.

Corresponds to Haskell's Data.Ix.Ix.

• range : α × α → List α

  Enumerate all indices in the range $[lo, hi]$. $$\text{range}(lo, hi) = [lo, lo+1, \ldots, hi]$$

• rangeSize : α × α → Nat

  The number of indices in the range. $$\text{rangeSize}(lo, hi) = |\text{range}(lo, hi)|$$

• index (bounds : α × α) : α → Option { n : Nat // n < rangeSize bounds }

  Map an index to its zero-based position in the range, bounded by rangeSize. $$\text{index}((lo, hi), i) = \begin{cases} \text{some}\langle i - lo, \_ \rangle & lo \leq i \leq hi \\ \text{none} & \text{otherwise} \end{cases}$$ The returned index carries a proof that it is less than rangeSize bounds.

• inRange : α × α → α → Bool

  Test whether an index is within the given bounds. $$\text{inRange}((lo, hi), i) \iff lo \leq i \leq hi$$

@[implicit_reducible]

instance Data.instIxNat : Ix Nat

Equations

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

@[implicit_reducible]

instance Data.instIxInt : Ix Int

Equations

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

@[implicit_reducible]

instance Data.instIxChar : Ix Char

Equations

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

@[implicit_reducible]

instance Data.instIxBool : Ix Bool

Equations

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

@[implicit_reducible]

instance Data.instIxProd {α : Type u_1} {β : Type u_2} [Ix α] [Ix β] : Ix (α × β)

Equations

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

theorem Data.Ix.inRange_iff_index_isSome_nat (bounds : Nat × Nat) (x : Nat) : inRange bounds x = (index bounds x).isSome

inRange is consistent with index: a value is in range iff index returns some. $$\text{inRange}(b, x) \iff \text{index}(b, x).\text{isSome}$$ For the Nat instance.