SWI-Prolog 7.6.4:
?- dif(X, f(Y)), X=f(a).
X = f(a),
dif(f(f(a), Y), f(f(Y), a)).
Note that I use f/1
in the query, but the constraint is on f/2
. It's not wrong, but seems rather circuitous. Why doesn't Prolog return
?- dif(X, f(Y)), X=f(a).
X = f(a),
dif(Y, a).
That f
in the printed constraint has nothing to do with your f
. It's just a placeholder to keep subterms together:
?- dif(X, incal(Y)), X=incal(a).
X = incal(a),
dif(f(incal(a), Y), f(incal(Y), a)). <--- residual constraints, not yet resolved
The above meaning just that:
incal(a)
must stay different from incal(Y)
; andY
must stay different from a
Yes, you could simplify that but ... when does one know whether optimization will cost less than one will gain?