On Mar 25 at 14:10 +0300, grechukbogdan wrote: > Suggestion 1. The message like “The current goal could be solved > directly with...” should appear not only after I formulate the > existing result as a lemma, but also when I formulate it inside the > proof, say after have. Ideally, something like this should work when > the existing result appears as a subgoal in the proof, etc. > > The first part of this (about “have”) I have suggested during my > first visit in June, and the reply was “good point. We will think > about it”. This is very important because it will help to avoid > duplicate job. Is it hard for realization? > > Unfortunately, this mechanism is very sensitive for reformulations. > For example, there exist a lemma “id x = x”, but I have no > suggestions for lemma “x = id x”. In this and many similar cases > Sledgehammer can help, but the same question arises: is it possible > to run it in the background automatically, every time when I > formulate a lemma or “have” statement? Manually running: find_theorems solves or C-c C-f solves should have the desired effect. You could also make a more specific key binding if you need this often. Tim.
Description: Digital signature