idris - 有证据表明转换有效时的 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

它的行为与标准 lib 函数相同，但不需要返回 aMaybe因为总是可以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在第二种情况下进行模式匹配（即使其值未在右侧使用），以便可以填写递归调用的自动参数。