아그다(Agda), 불리언 명제

Question

이것은 과제에 대한 서문입니다.첫 번째 질문에 대한 질문이 이미 요청되었습니다.따라서 데이터 유형은 다음과 같습니다.

data BoolProp : ??? where
  ptrue  : BoolProp true
  pfalse : BoolProp false
  pand   : (P Q : Bool) -> (BoolProp P) -> (BoolProp Q) -> BoolProp (P ??? Q)
  por    : (P Q : Bool) -> (BoolProp P) -> (BoolProp Q) -> BoolProp (P ??? Q)
  pnot   : (P : Bool) -> BoolProp (not P)

이제 우리는 제안서를 작성하라는 요청을 받고 있습니다.

eval (PAnd (POr PTrue PFalse) PFalse) 

반환해야 BoolProp false

나는 이것을 어떻게 해야 할지 혼란스러워지고 있습니다. Ptrue 보고 BoolProp true 그러나 데이터 유형의 경우 por 두 개를 받아들인다 Bool그렇지 않다 BoolProp'에스.데이터 유형이 잘못되었을 수 있습니다.무슨 일이 있어도 좋을 것 같아요

평가 코드는 하스켈 코드의 일부라는 점을 추가해야 합니다.

메모:모든 것을 공개하지 않도록 편집했습니다.

Answer 1

코드가 컴파일되지 않는 이유는 첫 번째 섹션의 괄호 안이 올바르지 않기 때문입니다.예를 들어, Pand의 경우 Pand와 같아야합니다.∀ { P Q :Bool } → BoolProp P → BoolProp Q → BoolProp (P ∧ Q )

이를 변경하면 두 번째 부분이 컴파일됩니다.나는 똑같은 문제를 겪었습니다....

Answer 2

글쎄, 나는 그것이 옳은지 아닌지에 몰라요. 그리고 이것은 마지막 질문에 대한 평가를 취하는 경우 첫 번째 부분을위한 것입니다.

하지만 첫 번째 부분에서는 유형 서명이 다음과 같기 때문에

prop : BoolProp false

방금 prop을 eval 문과 동일하게 만들었습니다.eval 문은 BoolProp과 동일해야 하기 때문입니다.

그래서

prop = (pand (por ptrue pfalse) pfalse)

잘못됐을지도 몰라 하지만 C-c C-l 및 C-c C-n

그리고 나는 행복하다.