日付を持たない時刻を扱う時計を実装しましょう。
その時計では、分を足したり引いたりできるようにします。
同じ時刻を表す2つの時計は、互いに等しくなければなりません。
この演習を完了するには、データ型Clockを定義し、BEqとToStringのインスタンスを追加し、次の関数を実装する必要があります。
createは、時間と分をそれぞれ表す、負の値もあり得る2つの整数を受け取り、有効なClockを生成します。addは、Clockと、そのClockの時刻に加算する分数を受け取り、新しいClockを生成します。subtractは、Clockと、そのClockの時刻から減算する分数を受け取り、新しいClockを生成します。Clock型は、"00:00"から"23:59"までの24時間制の時刻を表すことに注意してください。
Clockの時間と分にはそれぞれ上限と下限があることに注意してください:
0 <= hour < 240 <= minute < 60Leanでは、このような制約を型レベルで表現するのが慣用的で、そうすることで不正な値が_表現不可能_になります。 ただし、そのためには、与えられた値がこれらの制約を満たすことを_証明_する必要もあります。
もしやってみたいなら、このトピックの良い入門があります: