如何使Idris警告不完整的案件/比赛？

Question

例如，当为以下类型实现Show实例时：

data Shape = Circle Double
           | Box Vector2D
           | Polygon (List Vector2D)
           | Chain (List Vector2D)

...并且省略Chain大小写，Idris将成功键入check this file。

类似的问题用于实现其他功能。

在文件开头添加%default total似乎无济于事，但我的印象是应该这样做。

Answer 1

[您可以使用以下选项来呼叫idris：

-全部Require功能默认为总计

我仍然不确定这是否是唯一的方法，为什么%default total似乎什么也不做，以及是否有可能仅在一个函数不完整时才得到警告。