Perk

Ready to put your newfound language skills into use? Get 40% off CodeCrafter's real-world proficiency projects!

Claim your discount
Tracks
/
Lean
Lean
/
Exercises
/
Clock
Clock

Clock

Medium
OverviewCommunity Solutions

Instructions

Implement a clock that handles times without dates.

You should be able to add and subtract minutes to it.

Two clocks that represent the same time should be equal to each other.

Implementation

To complete this exercise you need to define the data type Clock, add a BEq and a ToString instance, and implement the functions:

  • create, that takes two integers, possibly negative, representing hours and minutes respectively, and creates a valid Clock.
  • add, that takes a Clock and a number of minutes to be added to the time in the Clock, generating a new Clock.
  • subtract, that takes a Clock and a number of minutes to be subtracted from the time in the Clock, generating a new Clock.

Note that the Clock type represents a 24 hour clock going from "00:00" to "23:59".

Advanced

Note that both the hours and the minutes in a Clock are bounded:

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

It is idiomatic in Lean to represent such constraints at the type level, so that invalid values are unrepresentable. However, this also requires proving that a given value satisfies these constraints.

If you are feeling up to it, here is a good introduction to this topic:

Source

Pairing session with Erin Drummond
Edit via GitHub The link opens in a new window or tab
Lean Exercism

Ready to start Clock?

Sign up to Exercism to learn and master Lean with 100 exercises, and real human mentoring, all for free.

Sign up, it’s free! Log in to Exercism