REL
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
Was this doc helpful?