haskell - Agda， bool 命题

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 )

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