1
슬레 드 해머를 사용할 때 어떻게 가정이나 일부 보조 정리를 피할 수 있습니까? 그렇게 할 거리가 있습니까? 내 sublemma를 해결할 다른 방법이나 보조 정리가 있다고 확신하기 때문에.슬레지 해머로 가정 피하기
A
답변
1
속성이 [no_atp] 인 사실은 Sledgehammer로 전달되지 않습니다. 따라서 보조 정리 또는 가정을 [no_atp]으로 선언하면 쓰레기 해머가 그들을 사용할 수 없어야합니다.