I need a "width," a length of vector to transfer between two functions. I managed to define a list with upper bound on its' length (ListLE n X) and I'd like to create a function that collect data in ListLE and answers Just (Vec n X) when it collected ListLE (width) X (and Nothing otherwise).
I cannot figure how to define it width. [let (----width : Nat)] elaborates to seemingly proper structure, but then I fail to figure out how to provide value for width. width [<= succ (succ zero)] elaborates to brown expression, telling me I'm wrong. But I don't see how and where I am wrong.
