当有证据表明转换将起作用时为natToFin
当有证据表明转换将起作用时为natToFin
提问于 2015-04-28 09:28:01
标准库中的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函数相同，但不需要返回Maybe，因为如果m大于m，则始终可以从n生成Fin n。
如何实现myNatToFin
回答 1
Stack Overflow用户
发布于 2015-04-28 09:43:02
您可以通过同时递归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进行模式匹配(即使在右侧没有使用它的值)，以便可以填充递归调用的自动参数。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/29908731
复制相关文章
相似问题
腾讯云开发者
