0

この回答を書いているときに、これが期待どおりに機能することに気付きました。

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

foo : Nat
foo = onlyModBy5 25

しかし、プロパティに名前を付けるとすぐに機能しなくなります:

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

引数を埋めるとauto失敗するようになりました

Can't find a value of type 
        Divides 5 25

Idris がDividesの定義を見抜くことができないのはなぜですか?

4

1 に答える 1

1

これが理由かどうかはわかりませんが、modNat は完全ではありません。それはイドリスをつまずかせる良い理由になるでしょう。

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

何らかの理由で、これもすでに失敗しています (元のバージョンから 1 回だけ間接化します)。

于 2016-04-11T15:19:41.533 に答える