Stream: new members
Topic: Pattern matching on arrays
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?
Kyle Miller (Jan 24 2021 at 19:01):
Is this what you mean?
def is_len_two : Array α → Bool | #[a, b] => true | _ => false
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:
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
Calvin Lee (Jan 24 2021 at 19:26):
On second thought I'll just pattern match on
Last updated: May 08 2021 at 09:11 UTC