将Nat保持在固定范围内

Question

我希望有一个Nat保持在固定范围内.我想要功能,如果他们要将数字推到范围之外incr,decr那就失败了.这似乎是一个很好的用例Fin,但我不确定如何使其工作.类型签名可能如下所示:

- Returns the next value in the ordered finite set.
- Returns Nothing if the input element is the last element in the set. 
incr : Fin n -> Maybe (Fin n)

- Returns the previous value in the ordered finite set.
- Returns Nothing if the input element is the first element in the set.
decr : Fin n -> Maybe (Fin n)

在Nat将被用于索引成Vect n.我如何实现incr和decr？是Fin即使是正确的选择呢？

Answer 1

我想最简单的方法是使用一些标准的 Fin\xe2\x86\x94Nat 转换函数Data.Fin：

\n\n

incr, decr : {n : Nat} -> Fin n -> Maybe (Fin n)\nincr {n=n} f = natToFin (succ $ finToNat f) n\n\ndecr {n=n} f = case finToNat f of\n    Z => Nothing\n    S k => natToFin k n\n

\n