How do I explicitly provide an implicit argument?
Suppose I have a function with this signature:
myNatToFin : (m : Nat) -> (n : Nat) -> { auto p : n `GT` m } -> Fin n
I am trying to apply it like this myNatToFin k (S k)
in the body of another function and I am getting the error:
Can't solve goal
GT (S k) k
So, I believe that I should explicitly pass the proof of that GT (S k) k
, but I have no idea how to do it. How can I explicitly pass the implicit proof argument so this will compile?
+3
source to share
1 answer
You can give explicit arguments for implicit parameters by enclosing them in curly braces and prefixes with the parameter name, for example {p = someExpression foo}
.
Complete example:
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}
+2
source to share