enums - 在 Idris 中，如何将 1 添加到 Fin 直到达到 "max"

我有一个数据类型，它在构造函数中接受一个数字，这个数字必须在 1 到 5 之间(表示为 0..4):

import Data.Fin
data Stars = MkStars (Fin 5)

我想创建一个将一个添加到现有 star 的函数，如果它已经是 5 stars ，则不执行任何操作

我试过了

addOneStar: Stars -> Stars
addOneStar (MkStars FZ) = MkStars (FS FZ)
addOneStar (MkStars (FS x)) = if x < 3
                              then MkStars (FS (FS x))
                              else MkStars (FS x)

但它没有编译错误:

Type mismatch between
            Fin 4 (Type of x)
    and
            Fin 3 (Expected type)

    Specifically:
            Type mismatch between
                    1
            and
                    0

有人可以向我解释为什么会出现这个错误吗？
以及如何修复它？

最佳答案

Fin 实现了 Enum 接口(interface)，为后继函数 succ 提供了所需的语义，这使得 addOneStar 的实现变得微不足道:

addOneStar: Stars -> Stars
addOneStar (MkStars s) = MkStars $ succ s