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....

Answer 2

well i dunno if it right or not and this is just for the first part if your taking about the eval on the last question, i dunno.

But for the first part since the type signature is

prop : BoolProp false

I just made prop equal to the eval statement. Since the eval statement should equal to BoolProp.

so

prop = (pand (por ptrue pfalse) pfalse)

maybe its wrong, i dunno but it C-c C-l and C-c C-n

and I am happy.