View for (mod n)

延續上一個 Bound View, 稍微修改之後, 再配合 \mathbb{Z}_n 結構, 可以得到一個對 \mathbb{N} 的模數 n 的 view。首先修改 Bound 為

data Bound (k : ℕ) : ℕ → Set where
below : (n : ℕ) → (l : ℕ) → (l+n=k : l + (suc n) ≡ k)
    → Bound k n
above : (n : ℕ) → (l : ℕ) → (l+k=n : l + k ≡ n) → Bound k n

亦即將 below 的條件改為 n < k,而 above 則是 n \geq k。toBound 根據此稍作修改。接下來是 \mathbb{Z}_n 的結構定義,因為要作成 \mathbb{N} 的 view,index 上放入自然數。

data Z (k : ℕ) : ℕ → Set where
 cl : (m : ℕ){m<k : (suc m) ≤ k} (n : ℕ) → Z k (m + (n * k))

接下來就是將自然數轉成 \mathbb{Z}_nContinue reading