الساعة

الساعة

متوسط

التعليمات

نفّذ ساعة تتعامل مع الأوقات بدون تواريخ.

ينبغي أن تكون قادرًا على إضافة دقائق إليها وطرحها منها.

ينبغي أن تتساوى ساعتان تمثلان الوقت نفسه.

التنفيذ

لإكمال هذا التمرين، عليك تعريف نوع البيانات Clock، وإضافة نسخة BEq ونسخة ToString، وتنفيذ الدوال التالية:

  • create، وهي تأخذ عددين صحيحين، قد يكونان سالبين، يمثلان الساعات والدقائق على التوالي، وتنشئ Clock صالحًا.
  • add، وهي تأخذ Clock وعددًا من الدقائق يُضاف إلى الوقت في Clock، فتنتج Clock جديدًا.
  • subtract، وهي تأخذ Clock وعددًا من الدقائق يُطرح من الوقت في Clock، فتنتج Clock جديدًا.

لاحظ أن نوع Clock يمثل ساعة بنظام 24 ساعة، تمتد من "00:00" إلى "23:59".

Advanced

لاحظ أن الساعات والدقائق في Clock كلتاهما محدودتان:

  • 0 <= hour < 24
  • 0 <= minute < 60

من الأساليب المألوفة في Lean تمثيل مثل هذه القيود على مستوى النوع، بحيث تصبح القيم غير الصالحة غير قابلة للتمثيل. لكن هذا يتطلب أيضًا إثبات أن قيمة معينة تحقق هذه القيود.

إذا كنت مستعدًا لذلك، فإليك مقدمة جيدة لهذا الموضوع:


المصدر

جلسة برمجة ثنائية مع Erin Drummond
تعديل عبر GitHub يفتح الرابط في نافذة أو علامة تبويب جديدة
Lean Exercism

مستعد لبدء الساعة؟

سجّل في Exercism لتتعلّم وتتقن Lean عبر 100 تمرين، وإرشاد بشري حقيقي، وكل ذلك مجانًا.