Underscore

Expr := "_"

Underscore is a variable without a name. The compiler rewrites it into the relation x: true, which is the infinite relation of all values. After further rewriting, this typically becomes an existentially quantified variable with a unique name. Underscore is mostly useful if you do not care about certain arguments of a relation and want to avoid introducing a named variable and quantifier.

For example:

// Unary relation of all orders with a line item:
o: line_item(o, _)
 
// There does not exist an order for customer c:
not(order_customer(_, c))
 
// Count the number of distinct values of a function or relation `f`:
count[f[_]]
 
// Get the second column of a ternary relation `P`:
def Q(x) = P(_, x, _)

You can achieve the same effect by replacing the underscore with Any.

Next: Existential Quantification