Pergunta
Um prefácio, note que esta é uma atribuição.Uma questão já foi perguntado sobre para a primeira pergunta.Por isso, temos o tipo de dados:
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)
Agora nós estamos sendo solicitados a escrever a proposição de
eval (PAnd (POr PTrue PFalse) PFalse)
qual deve retornar BoolProp
false
Eu Só estou ficando confuso sobre como fazer isso. Ptrue
retorna BoolProp true
no entanto, com o tipo de dados por
leva em dois Bool
's não BoolProp
's.Talvez o tipo de dados é errado.Qualquer heads up seria ótimo
Gostaria de acrescentar que o eval de código é um trecho do código haskell
nota:editado para não dar tudo de distância
Solução
O motivo seu código não é a compilação é porque o bracketing, em sua primeira seção é incorreto.Por exemplo, para o tipo deve ser como tipo :∀ { P, Q :Bool } → BoolProp P → BoolProp Q → BoolProp (P ∧ Q )
Alteração e a segunda parte deve compilar.Eu tinha exatamente o mesmo problema....
Outras dicas
bem, eu não sei se é certo ou não e esta é só a primeira parte se o seu tomando sobre o eval sobre a última pergunta, eu não sei.
Mas para a primeira parte, uma vez que o tipo de assinatura é
prop : BoolProp false
Eu apenas fiz prop igual a instrução eval.Desde a instrução eval deve ser igual a BoolProp.
então,
prop = (pand (por ptrue pfalse) pfalse)
talvez a sua errado, eu não sei mas C-c C-l e C-c C-n
e eu estou feliz.