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?


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

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}




All Articles