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

Die folgende Funktion wird kompiliert:

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

Aber was machtk repräsentiere mit seinemNat ** 5 * k = n Syntax

Auch wie kann ich es nennen? Folgendes habe ich versucht, aber ich verstehe die Ausgabe nicht.

*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

Quelle der Antwort -https: //groups.google.com/d/msg/idris-lang/ZPi9wCd95FY/eo3tRijGAAA