def String.vecToStr {n : Nat} : (Fin n → String) → String

Equations

• String.vecToStr x_2 = ""
• String.vecToStr s = if n = 0 then s 0 else s 0 ++ ", " ++ String.vecToStr fun (i : Fin n) => s i.succ