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}