def Nat.natToVec : ℕ → (n : ℕ) → Option (Fin n → ℕ)

Equations

• Nat.natToVec 0 0 = some ![]
• e.succ.natToVec n.succ = Option.map (fun (x : Fin n → ℕ) => (Nat.unpair e).1 :> x) ((Nat.unpair e).2.natToVec n)
• x✝¹.natToVec x✝ = none

@[simp]

theorem Nat.natToVec_vecToNat {n : ℕ} (v : Fin n → ℕ) : (Matrix.vecToNat v).natToVec n = some v

theorem Nat.lt_of_eq_natToVec {n e : ℕ} {v : Fin n → ℕ} (h : e.natToVec n = some v) (i : Fin n) : v i < e

@[irreducible]

def Nat.natToList : ℕ → List ℕ

List form of Nat.natToVec: the same decoding, with the length out of the type.

Equations

• Nat.natToList 0 = []
• e.succ.natToList = (Nat.unpair e).1 :: (Nat.unpair e).2.natToList

theorem Nat.natToVec_eq_some_iff {e k : ℕ} {v : Fin k → ℕ} : e.natToVec k = some v ↔ e.natToList = List.ofFn v

theorem Nat.natToVec_eq_none_of_length {e k : ℕ} (h : e.natToList.length ≠ k) : e.natToVec k = none

natToVec succeeds exactly when the length-free decoding has the expected length.

theorem Nat.natToVec_isSome_of_length {e k : ℕ} (h : e.natToList.length = k) : ∃ (v : Fin k → ℕ), e.natToVec k = some v