在编写这个答案时,我注意到,虽然这与预期一样有效:
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
arg失败
Can't find a value of type
Divides 5 25
为什么Idris不能看透Divides
的定义?
我不确定这是否是原因,但modNat不是总数。这将是绊倒idris的一个很好的理由。
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
由于某种原因,这也已经失败了(只是从原始版本间接地进行了一次)。