Pattern matching on arrays

Stream: new members

[Calvin Lee]

Is there any way to pattern match on arrays in lean 4?
I'm creating a vector types of arrays of a constant size. One thing I'd like to do is make this an instance of the functor class, however for this it's necessary to prove that map preserves the size of an array. I decided to go the route of creating my own "map" for arrays that generated this proof, but to do that I need to pattern match on arrays. Is there any way to do this?

[Kyle Miller]

Is this what you mean?

def is_len_two : Array α → Bool
| #[a, b] => true
| _ => false

[Calvin Lee]

yes, I think this would work (although I was thinking more like cons matching)
I was trying to pattern match on two terms at once, and it wasn't compiling because I didn't use a comma.... so I know my issue now :cry:

[Calvin Lee]

Would there be any way to prove that an array is nonempty given it doesn't match #[]?

[Calvin Lee]

On second thought I'll just pattern match on Array.isEmpty