@[inline]

def Fin.addNat? {n : Nat} (i : Fin n) (m : Nat) : Option (Fin n)

Overflow-aware addition of a natural number to an element of Fin n.

Examples:

• (2 : Fin 3).addNat? 1 = (none : Option (Fin 3))

• (2 : Fin 4).addNat? 1 = (some 3 : Option (Fin 4))

Equations

• i.addNat? m = if h : ↑i + m < n then some ⟨↑i + m, h⟩ else none

theorem Fin.addNat?_eq_some {n m : Nat} {i : Fin n} (h : ↑i + m < n) : i.addNat? m = some ⟨↑i + m, h⟩

theorem Fin.addNat?_eq_some_iff {n m : Nat} {j i : Fin n} : i.addNat? m = some j ↔ ↑i + m < n ∧ ↑j = ↑i + m

@[simp]

theorem Fin.addNat?_eq_none_iff {n m : Nat} {i : Fin n} : i.addNat? m = none ↔ n ≤ ↑i + m

@[simp]

theorem Fin.addNat?_zero {n : Nat} {i : Fin n} : i.addNat? 0 = some i

theorem Fin.addNat?_eq_dite {n m : Nat} {i : Fin n} : i.addNat? m = if h : ↑i + m < n then some ⟨↑i + m, h⟩ else none

@[deprecated Fin.addNat?_eq_dite (since := "2026-07-21")]

theorem Fin.addNat?_eq_dif {n m : Nat} {i : Fin n} : i.addNat? m = if h : ↑i + m < n then some ⟨↑i + m, h⟩ else none