   Go backward to 2.5 ValuesGo up to 2 Language ## 2.6 Predefined Predicates and Functions

The following predicates are predefined (`/n` denotes arity n):

`true/0`
The predicate denoting true.
```formula true;
> true.
```

`false/0`
The predicate denoting false.
```formula false;
> false.
```

`Set/1`
The predicate that returns true if and only if its argument is a set.
```formula Set({});
> true.
```

`Tuple/1`
The predicate that returns true if its argument is a tuple.
```formula Tuple(tuple(2, 3));
> true.
```

`Nat/1`
The predicate that returns true if its argument is a natural number.
```formula Nat(1);
> true.
```

`=/2`
The equality of values.
```formula =(2, +(1, 1));
> true.
```

`in/2`
The inclusion of an element (the first argument) in a set (the second argument).
```formula in(1, join(1, {}));
> true.
```

`<=/2`
The predicate on natural numbers that returns true if and only if its first argument is not larger than the second one.
```formula <=(1, 2);
> true.
```

Likewise the following functions are predefined:

`length/1`
The number of elements in a tuple.
```term length(tuple(2, 3));
> 2.
```
`{``}/0`
The empty set.
```term {};
> {}.
```
`join/2`
The function that returns the set that results from joining an element (the first argument) to a set (the second argument).
```term join (2, join(1, {}));
> {1, 2}.
```
`nat/2`
The interval of natural numbers from a lower bound (the first argument) up to and including an upper bound (the second argument).
```term nat(1, 10);
> 1..10.
term set(x in nat(1, 10): true, x);
> {1, 2, 3, 4, 5, 6, 7, 8, 9, 10}.
```
`+/2`
Addition on natural numbers.
```term +(7, 8);
> 15.
```
`*/2`
Multiplication on natural numbers.
```term *(2, 3);
> 6.
```
`-/2`
Subtraction of a natural number (the second argument) from another natural number (the first argument); the second argument must not be larger than the first one.
```term -(7, 8);
> ERROR: no such difference.
```

Maintained by: Wolfgang Schreiner
Last Modification: September 16, 2004   