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的。可能是数据类型不对。任何提醒都会很棒

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

笔记：对其进行了编辑，以免泄露所有内容

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)

也许是错误的，我不知道，但它是CC CL和CC CN

我很高兴。