أجدا، اقتراح منطقي

Question

ملاحظة تمهيدية أن هذا هو لمهمة.لقد تم بالفعل طرح سؤال حول السؤال الأول.لذلك لدينا نوع البيانات:

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'س.ربما نوع البيانات خاطئ.أي تنبيه سيكون رائعًا

يجب أن أضيف أن رمز التقييم هو مقتطف من كود هاسكل

ملحوظة:تم تحريره حتى لا يتخلى عن كل شيء

Answer 1

السبب وراء عدم ترجمة التعليمات البرمجية الخاصة بك هو أن الأقواس الموجودة في القسم الأول غير صحيحة.على سبيل المثال ، يجب أن يكون مثل pand:∀ { ف س :Bool } → BoolProp P → BoolProp Q → BoolProp (P ∧ Q )

قم بتغيير ذلك ويجب تجميع الجزء الثاني.كان لي بالضبط نفس المشكلة....

Answer 2

حسنًا ، أنا لا أفعل إذا كان ذلك صحيحًا أم لا ، وهذا هو فقط للجزء الأول إذا كنت تأخذ في السؤال الأخير على السؤال الأخير ، أنا لا أعرف.

ولكن بالنسبة للجزء الأول منذ نوع التوقيع

prop : BoolProp false

لقد قمت للتو بعمل دعامة مساوية لبيان التقييم.نظرًا لأن بيان التقييم يجب أن يساوي BoolProp.

لذا

prop = (pand (por ptrue pfalse) pfalse)

ربما من الخطأ ، أنا لا أعرف ولكنه cc cl و cc cn

وأنا سعيد.