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
```

source of answer - https://groups.google.com/d/msg/idris-lang/ZPi9wCd95FY/eo3tRijGAAAJ