Prob 2 in assignment 07

[ljw9111]

beq_id x y 를 사용할때

The term "beq_id x y" has type "bool" while it is expected to have type "Datatypes.bool".

이러한 에러가 발생합니다.

import 하는 bool이 다른것 같은데 혹시 이문제 해결방법 아시나요?

[aqjune]

안녕하세요. 혹시 어떤 상황에서 해당 에러가 났는지 알 수 있을까요? 제가 1번/2번을 푸는 중에는 해당 에러를 본 적이 없어서, 좀 더 정보가 필요할 것 같습니다. 감사합니다.

[ghost]

P02.v에서 t_update_permute을 증명하는데 Lemma beq_nat_true_iff를 사용했습니다. Coq 내에서는 에러 없이 잘 증명되었는데, make 작업을 하는데 subterm (?n:=?n1)을 못 찾는다는 메세지가 떴습니다.

Coq로 증명한 내용을 캡쳐해서 조교님 이메일로 같이 보내려는데, 확인 부탁드립니다.

조교님께 답변을 듣고 다시 수정하기에는 제출 시간이 지난 뒤라 클래임 제출이 어려울 것 같아, 확인 전에 미리 이메일 보내는 것에 대해서 양해 부탁드립니다 :)

이기웅 드림