idris - 如何显式提供隐式参数？

Question

假设我有一个带有这个签名的函数：

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

我尝试像这样myNatToFin k (S k)在另一个函数的主体中应用它，但出现错误：

Can't solve goal 
            GT (S k) k

所以，我相信我必须明确地通过一个证明GT (S k) k，但我不知道如何做到这一点。如何显式传递隐式证明参数以便编译？

Answer 1

您可以通过将隐式参数括在大括号中并在参数名称前加上前缀来为隐式参数提供显式参数，例如{p = someExpression foo}.

完整示例：

import Data.Fin

myNatToFin : (m : Nat) -> (n : Nat) -> { auto p : n `GT` m } -> Fin n
myNatToFin m n = ?x -- See https://stackoverflow.com/questions/29908731/

lteRefl : LTE n n
lteRefl {n = Z} = LTEZero
lteRefl {n = S _} = LTESucc lteRefl    

foo : (k : Nat) -> Fin (S k)
foo k = myNatToFin k (S k) {p = LTESucc lteRefl}