Solver for Linear Equalities
Example:
list : rational -> type.
nil : list 0.
, : rational -> list N -> list (N + 1). %infix right 100 ,.
append : list M -> list N -> list (M + N) -> type.
app_nil : append nil L2 L2.
app_cons : append (X , L1) L2 (X , L3) <- append L1 L2 L3.
?- L : list 3.
Solving...
Empty Substitution.
L = 0 , 0 , 0 , nil.
More? y
Empty Substitution.
L = 1 , 0 , 0 , nil.
Previous slide
Next slide
Back to first slide
View graphic version