تكتيكات المثل المخصص في إدريس

Question

إذا فهمت ذلك بشكل صحيح (أساسًا من وجود applyTactic دالة)، فمن الممكن كتابة تكتيكات مخصصة لمثبت النظرية في إدريس.ما (أو أين) بعض الأمثلة التي يمكنني استخدامها لتعلم كيفية القيام بذلك؟

Answer 1

هناك آليتان لكتابة التكتيكات المخصصة في إدريس:انعكاس عالي المستوى ومنخفض المستوى.

باستخدام الانعكاس عالي المستوى، يمكنك كتابة دالة تعمل على بناء الجملة بدلاً من البيانات المقيَّمة - ولن يؤدي ذلك إلى تقليل وسيطتها.تعيد هذه الوظائف تكتيكًا جديدًا، تم تحديده باستخدام التكتيكات الموجودة مسبقًا في إدريس.إذا كنت تريد إرجاع مصطلح إثبات مباشرة، فيمكنك دائمًا استخدامه Exact.يمكن العثور على مثال على هذا النوع من التأمل في مكتبة التأثيرات.يتم استدعاء تكتيكات التفكير عالية المستوى باستخدام byReflection في وضع الإثبات.

في التفكير منخفض المستوى، يمكنك العمل مباشرة مع المصطلحات المقتبسة من نظرية النوع الأساسي لإدريس.التكتيك إذن هو وظيفة في TT -> List (TTName, TT) -> Tactic حيث تكون الوسيطة الأولى هي نوع الهدف، والثانية هي سياق الإثبات المحلي، وتكون نتيجة الإرجاع هي نفسها كما في الانعكاس عالي المستوى.هذا ما ارتبط به الضحك فوق.يتم استدعاء هذه باستخدام applyTactic في وضع الإثبات.