ساعتی پیادهسازی کنید که زمان را بدون تاریخ مدیریت میکند.
باید بتوانید به آن دقیقه اضافه کنید و از آن دقیقه کم کنید.
دو ساعتی که یک زمان یکسان را نشان میدهند باید با هم برابر باشند.
برای کامل کردن این تمرین باید نوع دادهی Clock را تعریف کنید، یک نمونهی BEq و یک نمونهی ToString اضافه کنید و توابع زیر را پیادهسازی کنید:
create که دو عدد صحیح، که ممکن است منفی باشند، بهترتیب بهعنوان ساعت و دقیقه میگیرد و یک Clock معتبر میسازد.add که یک Clock و تعدادی دقیقه میگیرد، آن دقیقهها را به زمان موجود در Clock اضافه میکند و یک Clock جدید میسازد.subtract که یک Clock و تعدادی دقیقه میگیرد، آن دقیقهها را از زمان موجود در Clock کم میکند و یک Clock جدید میسازد.توجه کنید که نوع Clock یک ساعت ۲۴ساعته را نشان میدهد که از 00:00 تا 23:59 است.
توجه کنید که هم ساعت و هم دقیقه در یک Clock محدود هستند:
0 <= hour < 240 <= minute < 60در Lean رایج است که چنین محدودیتهایی را در سطح نوع نمایش دهند، طوری که مقادیر نامعتبر غیرقابل بازنمایی باشند. اما این کار همچنین نیازمند اثبات این است که یک مقدار مشخص این محدودیتها را برآورده میکند.
اگر آمادهاید، اینجا یک معرفی خوب دربارهی این موضوع هست: