3

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

4

2 に答える 2

6

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

于 2012-05-20T04:33:39.770 に答える
0

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.

于 2012-05-20T04:22:29.557 に答える