Zulip Chat Archive

Stream: new members

Topic: How to represent assertions about contents of lists?


aron (Jan 13 2025 at 21:00):

I want to represent certain assertions about lists, something like that the list in question contains at least 3 items for which a given predicate is true. Or at most 5 items for which it's true. Or exactly 2 items. Or anything in between.

But I'm struggling to think of how best to represent this sort of thing. As a refinement type containing a pair of list and predicate function, along with a proposition about (List.filter predicate list).length? As an inductive type representing the assertion? Or something else?

Edward van de Meent (Jan 13 2025 at 22:00):

I suspect the List.filter version will be the simplest way to do this.

Edward van de Meent (Jan 13 2025 at 22:01):

Particularly since that doesn't need lots of new API

Daniel Weber (Jan 16 2025 at 17:16):

You could also use docs#List.countP


Last updated: May 02 2025 at 03:31 UTC