3

前言注意这是一个作业。已经针对第一个问题提出了一个问题。所以我们有数据类型：

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's not BoolProp'。可能是数据类型错误。任何抬头都会很棒

我应该补充一点，eval 代码是 haskell 代码的一个片段

注意：对其进行了编辑以不放弃所有内容

4

2 回答 2

6

您的代码未编译的原因是因为您的第一部分中的括号不正确。例如，对于 pand 它应该像 pand ：∀ { PQ : Bool } → BoolProp P → BoolProp Q → BoolProp (P ∧ Q )

改变它，第二部分应该编译。我有完全相同的问题....

于 2012-05-20T04:33:39.770 回答
0

好吧，我不知道它是否正确，如果您对最后一个问题进行评估，这只是第一部分，我不知道。

但是对于第一部分，因为类型签名是

prop : BoolProp false

我只是让 prop 等于 eval 语句。由于 eval 语句应该等于 BoolProp。

所以

prop = (pand (por ptrue pfalse) pfalse)

也许它错了，我不知道，但它 Cc Cl 和 Cc Cn

我很高兴。

于 2012-05-20T04:22:29.557 回答