时钟

时钟

中等

说明

实现一个时钟,它能处理时间,但不涉及日期。

你应该能够给它加上或减去分钟数。

两个表示同一时间的时钟应该彼此相等。

实现

要完成这个练习,你需要定义数据类型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,全部免费。