there's a cheeky link to idris's vector type in the second paragraph: https://www.idris-lang.org/docs/idris2/current/base_docs/doc... which accomplishes just that