At-most quantifier

This quantifier checks whether a given condition is satisfied by no more than a specified number of elements in a collection.

Syntax

This quantifier has the following syntax:

at most /*<number>*/ of any /*<item>*/ in /*<collection>*/ satisfies /*<condition>*/

Either satisfy or satisfies can be used interchangeably:

at most /*<number>*/ of any /*<item>*/ in /*<collection>*/ satisfy /*<condition>*/

You can specify whether you want to consider only distinct elements:

at most /*<number>*/ of any distinct /*<item>*/ in /*<collection>*/ satisfies /*<condition>*/

You can also specify a name to refer to the index of the element in the collection:

at most /*<number>*/ of any /*<item>*/ in /*<collection>*/ indexed by /*<index>*/ satisfies /*<condition>*/

You must replace the /*<item>*/ and /*<index>*/ placeholders with a valid identifier. These variables will refer to the element and its index in the collection, as exemplified in the following section.

Examples

Here is an example that check whether at most two numbers in a collection are even:

at most 2 of any number in [2, 4, 6] satisfies number mod 2 is 0 // true

The following example checks whether the user added no more than two products over $50 after adding the first item to the cart:

at most 2 of any item in cart indexed by index satisfies item's price > 50 and index >= 1

Lastly, this example checks if a user has at most two distinct products of the category "Electronics" in their cart:

at most 2 of any distinct item in cart satisfies item's category is "Electronics"