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