我是Idris的新手,我試圖去捕捉基本概念和語法。Idris的'half'功能類型簽名
即使它聽起來毫無意義,我試圖定義一個將自然減半的half
函數。
我想拿出類似:
half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat)
但當然不工作。具體來說,我得到:
error: expected: dependent type signature
half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat)
這可能嗎?
謝謝。
嗯,謝謝,它確實是typechecks。無論如何,我想要表達的是類似「half:(n:Nat) - > Even n - > Nat」的信息,因爲生成的「Nat」實際上是第一個「Nat」的一半。在你的情況下,函數總數是多少(即只接受輸入甚至是'Nat')?你使用Eirther這個事實讓我覺得它不是,而在第一個版本中,我們必須提供一半帶有證明的'n',即偶數,這就省去了1,3和所有其他的奇數。再次感謝你的幫助。 –
第二個版本可以做成總數,因爲每個'n'都是'2 * k'或'2 * k + 1'。當然,第一個不能,因爲沒有'k',例如, '1 = 2 * k'。 – Cactus