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