agda - 带有模糊终止的条款

Question

我正在尝试在 agda 中定义二进制数，但 agda 看不到它⟦_⇑⟧正在终止。我真的不想打破可访问性关系。如何向 agda 显示 n 变小？

module Binary where

open import Data.Nat using (ℕ; _+_; +-suc)
open ℕ

2* : ℕ → ℕ
2* n = n + n

data Parity : ℕ → Set where
   : ∀ k → Parity (2* k)
   : ∀ k → Parity (1 + 2* k)

parity : ∀ n → Parity n
parity zero =  0
parity (suc n) with parity n
parity (suc .(k + k)) |  k =  k
parity (suc .(suc (k + k))) |  k rewrite sym (+-suc k k) =  (suc k)

data  : Set where
   : 
   :  → 
   :  → 

⟦_⇓⟧ :  → ℕ
⟦  ⇓⟧ = 0
⟦  b ⇓⟧ = 2* ⟦ b ⇓⟧
⟦  b ⇓⟧ = 1 + 2* ⟦ b ⇓⟧

⟦_⇑⟧ : ℕ → 
⟦ zero ⇑⟧ = 
⟦ suc n ⇑⟧ with parity n
⟦ suc .(k + k) ⇑⟧ |  k =  ⟦ k ⇑⟧
⟦ suc .(suc (k + k)) ⇑⟧ |  k =  ⟦ k ⇑⟧

错误：

Termination checking failed for the following functions:
  ⟦_⇑⟧
Problematic calls:
  ⟦ k ⇑⟧

标签： agdanon-termination

Answer 1