Suffices terminst advice

[HalflingHelper]

#42

[HalflingHelper]

Passing all tests, and I added two more where advice should / shouldn't be given. It might be worth taking some time to brainstorm more situations when this could arise, though as arguments of calls is certainly the most common.

[HalflingHelper]

Wait to merge this, there might be a problem with the operator fix :

suffices to prove:
        a + sum(d) = + a

[HalflingHelper]

Also the lalr parser doesn't like this :)
theorem foldr_eq_sum : all ls : List. sum(ls) = foldr(ls, 0, operator +)

[HalflingHelper]

It's the paren after operator+

[HalflingHelper]

Closing since 0e88ca9 appears to fix

[jsiek]

Interesting. You're solution is a more specific that what I just pushed, which could make it less verbose, which is good, but the question is whether Call is the only problematic context...

[jsiek]

I suspect that there are more contexts that could be problematic... any place in synthesis mode.

[jsiek]

So the really good solution would be to augment the substitute method to know about check/synthesis and only set inferred = False when substituting in a synthesis context. But that's a bunch more work. I'll make an issue for that.

[jsiek]

Hmm, actually, it's not as simple as recognizing synthesis mode because of generic functions.

[jsiek]

I think perhaps the fix I just pushed is good because it is conservative and not that complicated. To do better seems to require a much more complex solution.