날짜 없이 시간을 다루는 시계를 구현해요.
이 시계에 분을 더하거나 뺄 수 있어야 해요.
같은 시간을 나타내는 두 시계는 서로 같아야 해요.
이 연습 문제를 완료하려면 Clock 데이터 타입을 정의하고, BEq와 ToString 인스턴스를 추가하고, 다음 함수를 구현해야 해요.
create는 음수일 수도 있는 정수 두 개를 각각 시와 분으로 받아서 유효한 Clock을 만들어요.add는 Clock과, 그 Clock의 시각에 더할 분 수를 받아 새로운 Clock을 만들어요.subtract는 Clock과, 그 Clock의 시각에서 뺄 분 수를 받아 새로운 Clock을 만들어요.Clock 타입은 "00:00"부터 "23:59"까지 가는 24시간 시계를 나타낸다는 점에 유의해요.
Clock의 시와 분은 모두 범위가 제한되어 있어요.
0 <= hour < 240 <= minute < 60Lean에서는 이런 제약을 타입 수준에서 표현해서 잘못된 값이 _표현 불가능_하도록 만드는 것이 관용적이에요. 하지만 그러려면 주어진 값이 이런 제약을 만족한다는 것을 _증명_해야 해요.
한번 도전해 보고 싶다면, 이 주제를 다룬 좋은 입문 자료가 있어요.