理解`K：納特** 5 * K = N`簽名

Question

下面的函數編譯：

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

但到底是什麼k代表其Nat ** 5 * k = n語法？

另外，我怎樣稱呼它？這是我的嘗試，但我不明白輸出。答案的

*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 

源 - https://groups.google.com/d/msg/idris-lang/ZPi9wCd95FY/eo3tRijGAAAJ

Answer 1

(k : Nat) ** (5 * k = n)是從屬對由

• 第一元件k : Nat
• 第二元件prf : 5 * k = n

換句話說，這是一種存在類型，表示「存在一些k : Nat，例如5 * k = n」。建設性的，你必須給出這樣一個k和證明它確實滿足5 * k = n。

在你的榜樣，如果部分應用onlyModByFive到5，你會得到類型

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

的東西，所以第二個參數必須是(k : Nat) ** (5 * k = 5)類型。只有一種選擇的k我們可以在這裏做，將其設置爲1，並且證明5 * 1 = 5：

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

這工作，因爲5 * 1減少了5，所以我們必須證明5 = 5，可平凡完成直接使用Refl : a = a（統一a ~ 5）。