search

LPCIC / elpi

Embeddable Lambda Prolog Interpreter
GNU Lesser General Public License v2.1
273 stars 32 forks source link

bug in unification #218

Closed gares closed 5 months ago

gares commented 5 months ago 
$ elpi
goal> pi x\ (w\ f (y\ X x y) w) = (z\ X x z).

Success:
  X = c0 \ c1 \ f (c2 \ X0 c0 c2) c1
gares commented 5 months ago 
goal> (w\ f (y\ X y) w) = (z\ X z).  % works
goal> f (y\ X y) = (z\ X z).  % fails (that is intended)
gares commented 5 months ago 
pi w \ f (y\ X y) w = X w.  % works