I rarely feel the need for answer literals, i.e. to let provers
synthesize terms for me. And I doubt it would often work (although in
that paper they do benefit from it). Given that Sledgehammer is not a
trivial piece of engineering, I would not want to burden it with more
"proactive" functionality
Thanks for reminding me of this paper. It states that the modified version of
SPASS implements answer literals, which would allow sledgehammer for the first
time to handle variables in subgoals. This could be quite useful. What do
others think?
Of course, we would also have to consider the exte
