diff --git a/Kernel/Term.hpp b/Kernel/Term.hpp index 5d3be564e..51c415bf0 100644 --- a/Kernel/Term.hpp +++ b/Kernel/Term.hpp @@ -1078,7 +1078,7 @@ class Literal template unsigned hash() const { - return Literal::literalHash(functor(), polarity() ^ flip, + return Literal::literalHash(functor(), polarity() ^ flip, [&](auto i) -> TermList const& { return *nthArgument(i); }, arity(), someIf(isTwoVarEquality(), [&](){ return twoVarEqSort(); })); } @@ -1087,7 +1087,7 @@ class Literal static unsigned literalEquals(const Literal* lit, unsigned functor, bool polarity, GetArg getArg, unsigned arity, Option twoVarEqSort) { if (functor != lit->functor() || polarity != lit->polarity()) return false; - if (functor == 0) { + if (functor == 0) { // i.e., isEquality ASS_EQ(arity, 2) ASS(rightArgOrder(getArg(0), getArg(1))) ASS(rightArgOrder(*lit->nthArgument(0), *lit->nthArgument(1))) @@ -1107,7 +1107,7 @@ class Literal template static unsigned literalHash(unsigned functor, bool polarity, GetArg getArg, unsigned arity, Option twoVarEqSort) { - if (functor == 0) { + if (functor == 0) { // i.e., isEquality ASS_EQ(arity, 2) ASS(rightArgOrder(getArg(0), getArg(1))) return HashUtils::combine(