Как указать неявный аргумент явно?

Предположим, у меня есть функция с такой сигнатурой:

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, но я понятия не имею, как это сделать. Как я могу явно передать аргумент неявного доказательства, чтобы это скомпилировалось?


idris
person mushroom    schedule 28.04.2015    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Вы можете указать явные аргументы для неявных параметров, заключив их в фигурные скобки и добавив префикс имени параметра, например {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}
person Cactus    schedule 28.04.2015