isar

4열

1답변

Isar 증명에서`presume`을 언제 사용 하시겠습니까?

Isar에는 assume 외에 presume 명령을 사용하여 Isar 증명 블록에 사실을 소개합니다. 내가 볼 수 있고 문서에서 읽을 수있는 것으로부터 가정 (추정?)을 명시 적으로 목표에 나열 할 필요가 없으며 가정 된 진술이 다른 목표에서 따름을 보여주는 사례를 추가하는 것으로 보입니다. 질문은 다음과 같습니다. 대신 assume을 사용하고, presu