# Understanding `k : Nat ** 5 * k = n` Signature

2

The following function compiles:

``````onlyModByFive : (n : Nat) -> (k : Nat ** 5 * k = n) -> Nat
onlyModByFive n k = 100
``````

But what does `k` represent with its `Nat ** 5 * k = n` syntax?

Also, how can I call it? Here's what I tried, but I don't understand the output.

``````*Test> onlyModByFive 5 5
When checking an application of function Main.onlyModByFive:
(k : Nat ** plus k (plus k (plus k (plus k (plus k 0)))) = 5) is not a
numeric type
``````

5

`(k : Nat) ** (5 * k = n)` is a dependent pair consisting of

• A first element `k : Nat`
• A second element `prf : 5 * k = n`

In other words, this is an existential type that says "there exists some `k : Nat` such that `5 * k = n`". To be constructive, you must give such a `k` and a proof that it indeed satisfies `5 * k = n`.

In your example, if you partially apply `onlyModByFive` to `5`, you get something of type

``````onlyModModByFive 5 : ((k : Nat) ** (5 * k = 5)) -> Nat
``````

so the second argument has to be of type `(k : Nat) ** (5 * k = 5)`. There is only one choice of `k` we can make here, by setting it to `1`, and proving that `5 * 1 = 5`:

``````foo : Nat
foo = onlyModByFive 5 (1 ** Refl)
``````

This works because `5 * 1` reduces to `5`, so we have to prove `5 = 5`, which can be trivially done by using `Refl : a = a` directly (unifying `a ~ 5`).