Die folgende Funktion erstellt:Verständnis `k: Nat ** 5 * k = n 'Signature
onlyModByFive : (n : Nat) -> (k : Nat ** 5 * k = n) -> Nat
onlyModByFive n k = 100
Aber was bedeutet k
repräsentiert mit ihrer Nat ** 5 * k = n
Syntax?
Auch, wie kann ich es nennen? Hier ist, was ich versucht habe, 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/eo3tRijGAAAJ
Danke, Kaktus. Aber ich denke, dass mein def von 'onlyModByFive' ungültig ist, da es überhaupt keinen' mod' beinhaltet, nein? Ich fragte dieses Follow-up: http://stackoverflow.com/questions/36531852/function-to-determinine-if-nat-is-divisible-by-5-at-compile-time. –
Auch - könnten Sie bitte irgendwelche Lesungen auf der Beweis bezogenen 'Refl 'empfehlen, die Sie notiert hatten? –
@KevinMeredith könnten Sie beginnen, indem Sie lesen http://jozefg.bitbucket.org/posts/2014-08-06-equality.html und zur Kenntnis nehmen, dass wir hier über intensional propositional Gleichheit sprechen. – Cactus