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.
// 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
Next: Existential Quantification
Was this doc helpful?