Ragged arrays

ragged.idr

import Data.Vect
  
data Ragged : List Nat -> Type -> Type where
     Nil : Ragged [] a
     (::) : Vect n a -> Ragged ns a -> Ragged (n :: ns) a
       
test_ragged : Ragged [1,3,2] String
test_ragged = [["Foo"],
               ["Bar", "Baz", "Quux"],
               ["Thurlingdrome", "Bananas"]]