Agda, Boolean Proposition

Question

A foreword note that this is for an assignment. A question has already been asked about for the first question. So we have the data type:

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)

Now we're being asked to write the proposition

eval (PAnd (POr PTrue PFalse) PFalse) 

which should return BoolProp false

I'm Just getting confused on how to do this. Ptrue returns BoolProp true however with the data type por takes in two Bool's not BoolProp's. Maybe the data type is wrong. Any heads up would be great

I should add that the eval code is a snippet from the haskell code

note: editted it to not give everything away

Answer 1

The reason your code is not compiling is because the bracketing in your first section is incorrect. For example, for pand it should be like pand : ∀ { P Q : Bool } → BoolProp P → BoolProp Q → BoolProp (P ∧ Q )

Change that and the second part should compile. I had exactly the same problem....