阿格达,布尔命题

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 trueporBoolBoolProp

我应该补充说,eval代码是haskell代码的一个片段

注意:编辑它不会让一切都消失

Answer 1

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

改变那个,第二部分应该编译.我有完全相同的问题....