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}