避免與大錘假設

Question

請問我如何避免使用slegghammer時的一些假設或一些引理？有沒有這樣做？因爲我確信有另外的方法或引理來解決我的難題。

Answer 1

以屬性[no_atp]標記的事實不會傳遞給大錘。所以如果你用[no_atp]聲明你的引理或假設，那麼大錘就不應該能夠使用它們。