title: Meaning of -> in swi-prolog
body: <p>I have a program in swi-prolog and there is an operator(?) <strong>-></strong>, which I have met for the first time and I don't know what it is doing. There is a fragment of code, which I don't understand:</p>
  
  <pre><code>swf([PP-&gt;Q|F], [PP|L], X):- swf(F, L, X), axioms(X, PP-&gt;Q, F).
  </code></pre>
  
  <p>I found that when we have</p>
  
  <pre><code>X -&gt; Y ; Z
  </code></pre>
  
  <p>then if X is true then Y is executed, otherwise Z. But I don't see how it works in the case shown above.</p>
  
  <p>Thanks in advance.</p>
  
  <p>EDIT:</p>
  
  <p>To be honest, this is a part of computer-aided proof of Arrow's theorem (more precisely - the base case), this is entire code (from Proving Arrow’s theorem by PROLOG, Kenryo Indo):</p>
  
  <pre><code>p(Q) :- permutation(Q, [a, b, c]).
  
  p((X, Y), Q) :- p(Q), append(_, [X|B], Q), member(Y, B).
  
  pp((Q1,Q2)) :- p(Q1), p(Q2).
  
  all_pp(L) :- findall(QQ, pp(QQ), L).
  
  axioms(arrow, V, F) :- p(Q), V=(PP-&gt;Q), pareto(V), iia(V, F).
  
  swf([], [], _).
  swf([PP-&gt;Q|F], [PP|L], X):- swf(F, L, X), axioms(X, PP-&gt;Q, F).
  swf(F, X) :- all_pp(L), swf(F, L, X).
  
  pp(XY, agree, (Q1,Q2)) :- p(XY, Q1), p(XY, Q2).
  pp((X, Y), opposite, (Q1, Q2)) :- p((X, Y), Q1), p((Y, X), Q2).
  
  pareto(PP-&gt;R) :- \+ (pp(XY, agree, PP), \+ p(XY, R)).
  
  dictator(J, F) :- member(J:PP, [1:(P, _), 2:(_, P)]),
  \+ (member(PP-&gt;R, F), pp(_, opposite, (P, R))).
  
  
  agree(+, XY, QQ) :- pp(XY, agree, QQ).
  agree(-,(X,Y), QQ) :- pp((Y, X), agree, QQ).
  
  iia(PP-&gt;R, F) :- \+ (F \= [], pp(XY, A, PP), member(QQ-&gt;S, F),
  pp(XY, A, QQ), \+ agree(_, XY, (R, S))).
  </code></pre>
  
  <p>Still, I don't know how to treat ->. There is a chain of usages of X->Y: swf - axioms - pareto and swf - iia - member.</p>