通りました。疑ってすいませんでした。
summer school library っていうのを使ったら動きました。あとでライブラリのコードを読まねば。
module Views where open import Data.Nat data Parity : ℕ -> Set where even : (k : ℕ) -> Parity (k * 2) odd : (k : ℕ) -> Parity (1 + (k * 2)) parity : (n : ℕ) -> Parity n parity zero = even zero parity (suc n) with parity n parity (suc .(k * 2)) | even k = odd k parity (suc .(1 + (k * 2))) | odd k = even (suc k)