# Functional Modelling System

## Sets

The set constructs are the last fundamental part of the language. Up to now we have only encountered enumerations like `{"a","c"}` and ranges like `{1..5}`.

IDP4 supports more advanced set expressions. In a set you can write down a double pipe `||` and after that you can write a number of different things:

• `a <- s`, picks a new variable `a` out of a set. This variable can then be used in the members of the set. It behaves a lot like a for-loop. `{2*a || a <- s}` contains the double of all the elements of a set `s`.
• `a < 5`, any Boolean expression is seen as a guard that limits the content of the set. `{a || a <- s, a < 5}` is the set containing of all numbers in `s` which are smaller than 5.
• `a := 8`, behaves like a local let expression, `{a || a := 8}` is the singleton set of 8.
Sets

Note that these expressions are order dependent, as you can use the variables introduced in one expression in the next one. Look for at example at a definition of union

Sets

When you take the union of 2 sets `a` and `b` this can be done through first selecting a set `s` out of the two. And then taking all elements `x` in this set.

## Builtins

There are a few builtins over sets predefined.

• quantifiers: forall (`!`) and exists (`?`)
• `member`: membership test
• `count`: returns the cardinality of a set
• `sum` : returns the sum of the members of a set
• `sumBy` : returns the sum of the members of a set based on the result of a function
• `min`: returns the minimum of the members of a set
• `max`: returns the maximum of the members of a set
Set Builtins

## The other way around

Just like `element of` you can declare a symbol `subset of` and let IDP4 search for a set.

Uninterpreted Set