Zulip Chat Archive

Stream: new members

Topic: Pattern matching on arrays


view this post on Zulip Calvin Lee (Jan 24 2021 at 17:30):

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?

view this post on Zulip Kyle Miller (Jan 24 2021 at 19:01):

Is this what you mean?

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

view this post on Zulip Calvin Lee (Jan 24 2021 at 19:08):

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:

view this post on Zulip Calvin Lee (Jan 24 2021 at 19:17):

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

view this post on Zulip Calvin Lee (Jan 24 2021 at 19:26):

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


Last updated: May 08 2021 at 09:11 UTC