Треки
/
Lean
Lean
/
Вправи
/
Годинник
Годинник

Годинник

Середня

Вказівки

Реалізуйте годинник, який працює з часом без дат.

Потрібно вміти додавати хвилини до годинника й віднімати їх від нього.

Два годинники, які показують той самий час, мають бути рівними один одному.

Реалізація

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

Якщо відчуваємо в собі сили, ось гарний вступ до цієї теми:


Джерело

Сесія парного програмування з Ерін Драммонд
Редагувати через GitHub Посилання відкривається в новому вікні або вкладці
Lean Exercism

Час розпочати Годинник?

Зареєструйтеся на Exercism, щоб вивчати й опановувати Lean, а також 100 вправ та справжнє наставництво від людей, і все це безкоштовно.