시계

시계

보통

지침

날짜 없이 시간을 다루는 시계를 구현해요.

이 시계에 분을 더하거나 뺄 수 있어야 해요.

같은 시간을 나타내는 두 시계는 서로 같아야 해요.

구현

이 연습 문제를 완료하려면 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에 가입하고 Lean 트랙을 연습 문제 100개, 그리고 실제 사람의 멘토링과 함께 배우고 익혀 보세요. 모두 무료예요.