時鐘

時鐘

中等

說明

實作一個時鐘,用來處理不含日期的時間。

你應該要能對它加上或減去分鐘。

兩個代表相同時間的時鐘應該彼此相等。

實作

完成這個練習時,你需要定義資料型態Clock,加入BEq與ToString實例,並實作以下幾個函式:

  • create,接受兩個整數(可能為負數),分別代表小時與分鐘,並建立一個有效的 Clock。
  • add,接受一個 Clock 和要加到該 Clock 時間上的分鐘數,並產生一個新的 Clock。
  • subtract,接受一個 Clock 和要從該 Clock 時間減去的分鐘數,並產生一個新的 Clock。

請注意,Clock 型別代表從「00:00」到「23:59」的 24 小時制時鐘。

Advanced

請注意,Clock中的小時與分鐘都有範圍限制:

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

在 Lean 中,慣用的做法是在型別層級表示這類限制,讓無效的值_無法表示_。 不過,這也代表你得_證明_某個值確實符合這些限制。

如果你想試試看的話,這裡有這個主題不錯的入門介紹:


出處

與 Erin Drummond 的結對工作階段
透過 GitHub 編輯 連結會在新視窗或分頁中開啟
Lean Exercism

準備好開始 時鐘 了嗎?

註冊 Exercism,透過 100 個練習 和真人引導來學習並精通 Lean,全部免費。