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

Question

La fonction suivante compile:

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

Mais qu'est-ce que k représente avec sa syntaxe Nat ** 5 * k = n?

Aussi, comment puis-je l'appeler? Voici ce que j'ai essayé, mais je ne comprends pas la sortie.

*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 de réponse - https://groups.google.com/d/msg/idris-lang/ZPi9wCd95FY/eo3tRijGAAAJ

Answer 1

(k : Nat) ** (5 * k = n) est une paire dépendante constitué par

• Un premier élément k : Nat
• Un second élément prf : 5 * k = n

En d'autres termes, c'est un type existentiel qui dit "il existe quelques k : Nat tels que 5 * k = n". Pour être constructif, vous devez donner un tel k et une preuve qu'il satisfait en effet 5 * k = n.

Dans votre exemple, si vous appliquez partiellement onlyModByFive-5, vous obtenez quelque chose de type

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

de sorte que le second argument doit être de type (k : Nat) ** (5 * k = 5). Il n'y a qu'un seul choix de k nous pouvons faire ici, en mettant à 1, et prouver que 5 * 1 = 5:

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

Cela fonctionne parce que 5 * 1 réduit à 5, donc nous devons prouver 5 = 5, qui peut être fait trivialement en utilisant Refl : a = a directement (en unifiant a ~ 5).