当有证据证明转换有效时,natToFin

Question

在natToFin从标准库函数具有以下特征:

natToFin : Nat -> (n : Nat) -> Maybe (Fin n)

natToFin 4 5返回Just (FS (FS (FS (FS FZ)))) : Maybe (Fin 5),同时 natToFin 5 5返回Nothing.

我想要一个具有以下签名的函数:

myNatToFin : (m : Nat) -> (n : Nat) -> { auto p : n `GT` m } -> Fin n

它的行为一样的标准库函数,但并不需要返回Maybe,因为它总是能够产生一个Fin n从m考虑到n大于m.

我该如何实施myNatToFin？

Answer 1

您可以直接通过递归上做到这一点m,n以及证据n `GT` m的同时:

import Data.Fin

myNatToFin : (m : Nat) -> (n : Nat) -> {auto p : n `GT` m} -> Fin n
myNatToFin Z (S n) = FZ
myNatToFin (S m) (S n) {p = LTESucc _} = FS $ myNatToFin m n

请注意,您需要p在第二种情况下进行模式匹配(即使其值未在右侧使用),以便可以填充递归调用的自动参数.