這個'with'塊爲什麼會破壞這個函數的整體性？

Question

我試圖計算奇偶校驗與半的地板一起，在自然數：

data IsEven : Nat -> Nat -> Type where 
    Times2 : (n : Nat) -> IsEven (n + n) n 

data IsOdd : Nat -> Nat -> Type where 
    Times2Plus1 : (n : Nat) -> IsOdd (S (n + n)) n 

parity : (n : Nat) -> Either (Exists (IsEven n)) (Exists (IsOdd n)) 

我試着具有明顯的執行parity打算：

parity Z = Left $ Evidence _ $ Times2 0 
parity (S Z) = Right $ Evidence _ $ Times2Plus1 0 
parity (S (S n)) with (parity n) 
    parity (S (S (k + k))) | Left (Evidence _ (Times2 k)) = 
     Left $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2 (S k) 
    parity (S (S (S ((k + k))))) | Right (Evidence _ (Times2Plus1 k)) = 
     Right $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2Plus1 (S k) 

這typechecks和工作原理預期。但是，如果我嘗試標記parity爲total，伊德里斯開始抱怨：

parity is possibly not total due to: with block in parity 

唯一with塊我在parity看到的是一個從parity (S (S n))到parity n遞歸調用，但顯然是有理有據的，因爲n在結構上比S (S n)小。

我如何說服伊德里斯認爲parity是總數？

Answer 1

它看起來像我的錯誤，因爲基於case以下解決方案通過了全部檢查：

total 
parity : (n : Nat) -> Either (Exists (IsEven n)) (Exists (IsOdd n)) 
parity Z = Left $ Evidence _ $ Times2 0 
parity (S Z) = Right $ Evidence _ $ Times2Plus1 0 
parity (S (S k)) = 
    case (parity k) of 
    Left (Evidence k (Times2 k)) => 
     Left $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2 (S k) 
    Right (Evidence k (Times2Plus1 k)) => 
     Right $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2Plus1 (S k)