Zulip Chat Archive

Stream: std4

Topic: Array lemmas


Matej Penciak (Oct 26 2022 at 02:43):

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 (Oct 26 2022 at 02:47):

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

Matej Penciak (Oct 26 2022 at 03:12):

Mario Carneiro said:

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

Hmmm, I suppose that's a valid answer


Last updated: Dec 20 2023 at 11:08 UTC