这个'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)