Реалізуйте годинник, який працює з часом без дат.
Потрібно вміти додавати хвилини до годинника й віднімати їх від нього.
Два годинники, які показують той самий час, мають бути рівними один одному.
Щоб виконати цю вправу, визначте тип даних 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 ідіоматично представляти такі обмеження на рівні типу, щоб некоректні значення були непредставними. Однак це також вимагає доведення, що задане значення задовольняє ці обмеження.
Якщо відчуваємо в собі сили, ось гарний вступ до цієї теми: