Auto implizite arg nicht mehr funktioniert, wenn Art einen Namen

Question

gegeben Während this answer schreiben, bemerkte ich, dass dies zwar wie erwartet funktioniert:

onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat 
onlyModBy5 n = n 

foo : Nat 
foo = onlyModBy5 25 

aber sobald ich einen Namen für die Eigenschaft geben sie nicht mehr funktioniert:

Divides : Nat -> Nat -> Type 
Divides n k = k `modNat` n = 0 

onlyModBy5 : (n : Nat) -> {auto prf : 5 `Divides` n} -> Nat 
onlyModBy5 n = n 

foo : Nat 
foo = onlyModBy5 25 

jetzt die auto arg Füllung nicht mit

Can't find a value of type 
     Divides 5 25 

Warum kann Idris die Divides Definition nicht sehen?

Answer 1

Ich bin mir nicht sicher, ob das der Grund ist, aber modNat ist nicht total. Das wäre ein guter Grund, Idris zu stolpern.

divides : Nat -> Nat -> Nat 
divides n k = n `modNat` k 

onlyModBy5 : (n : Nat) -> {auto prf : n `divides` 5 = 0 } -> Nat 
onlyModBy5 n = n 

foo : Nat 
foo = onlyModBy5 25 

Aus irgendeinem Grund schlägt dies auch schon fehl (nur einmal von der ursprünglichen Version ableitend).