نفّذ ساعة تتعامل مع الأوقات بدون تواريخ.
ينبغي أن تكون قادرًا على إضافة دقائق إليها وطرحها منها.
ينبغي أن تتساوى ساعتان تمثلان الوقت نفسه.
لإكمال هذا التمرين، عليك تعريف نوع البيانات Clock، وإضافة نسخة BEq ونسخة ToString، وتنفيذ الدوال التالية:
create، وهي تأخذ عددين صحيحين، قد يكونان سالبين، يمثلان الساعات والدقائق على التوالي، وتنشئ Clock صالحًا.add، وهي تأخذ Clock وعددًا من الدقائق يُضاف إلى الوقت في Clock، فتنتج Clock جديدًا.subtract، وهي تأخذ Clock وعددًا من الدقائق يُطرح من الوقت في Clock، فتنتج Clock جديدًا.لاحظ أن نوع Clock يمثل ساعة بنظام 24 ساعة، تمتد من "00:00" إلى "23:59".
لاحظ أن الساعات والدقائق في Clock كلتاهما محدودتان:
0 <= hour < 240 <= minute < 60من الأساليب المألوفة في Lean تمثيل مثل هذه القيود على مستوى النوع، بحيث تصبح القيم غير الصالحة غير قابلة للتمثيل. لكن هذا يتطلب أيضًا إثبات أن قيمة معينة تحقق هذه القيود.
إذا كنت مستعدًا لذلك، فإليك مقدمة جيدة لهذا الموضوع: