Array lemmas

Stream: std4

[Matej Penciak]

Hey everyone

I've been trying to collect a list of lemmas that are missing for arrays that are useful for lists, and I'm having a hard time coming up with a comprehensive list.

When I was trying to get fixed-length arrays to work in a project I was working on one of the big stumbling blocks I ran into was a need for a lemma along the lines of Array.size_zipWith (which says something equivalent to List.length_zipWith), so that's going on the list... But other than that, I'm having a hard time comparing the list of List (haha :neutral:) lemmas that are not known for Array).

It'd be nice to collect a list of big targets that we should aim for to get feature parity between arrays and lists, and I'd be curious to see what other results people would like to see. After a couple days I'll compile the stuff from this thread and make an issue in std4 to give myself/others goals to work towards.

[Mario Carneiro]

Why isn't the answer "all of the lemmas"?

[Matej Penciak]

Mario Carneiro said:

Why isn't the answer "all of the lemmas"?

Hmmm, I suppose that's a valid answer