Агда, логическое предложение

В предисловии обратите внимание, что это для задания. Вопрос по первому вопросу уже задан. Итак, у нас есть тип данных:

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.

примечание: отредактировал, чтобы не выдавать все


haskell agda
person Abstract    schedule 20.05.2012    source источник
comment
лол, это как-то напрягает, а не пора ли нам в 12   -  person rissicay    schedule 20.05.2012
comment
лучше поздно, чем никогда, но все же ваш ответ не слишком полезен. и я начал это вчера утром   -  person Abstract    schedule 20.05.2012
comment
хаха да это не так. Я тоже только начал, очевидно, я тоже пытался найти ответ в Google и оказался здесь.   -  person rissicay    schedule 20.05.2012
comment
ой извините, да давайте надеяться, что кто-то может дать ответ.   -  person Abstract    schedule 20.05.2012

Ответы (2)


arrow_upward
5
arrow_downward

Причина, по которой ваш код не компилируется, заключается в том, что скобки в вашем первом разделе неверны. Например, для pand это должно быть похоже на pand : ∀ { P Q : Bool } → BoolProp P → BoolProp Q → BoolProp (P ∧ Q )

Измените это, и вторая часть должна скомпилироваться. У меня была точно такая же проблема....

person anonymous    schedule 20.05.2012

arrow_upward
0
arrow_downward

ну, я не знаю, правильно это или нет, и это только для первой части, если вы думаете об оценке последнего вопроса, я не знаю.

Но для первой части, поскольку сигнатура типа

prop : BoolProp false

Я только что сделал prop равным оператору eval. Поскольку оператор eval должен быть равен BoolProp.

so 

prop = (pand (por ptrue pfalse) pfalse)

может быть это неправильно, я не знаю, но это C-c C-l и C-c C-n

И я рад.

person rissicay    schedule 20.05.2012
comment
вы уверены? потому что, когда я сделал это, я получил ошибку (BoolType true) !=‹ Bool типа Set при проверке того, что выражение ptrue имеет тип Bool. Вы точно использовали код, который я выложил, или немного изменили его? - person Abstract; 20.05.2012