Agda 練習中です

Agda を勉強中です。いわゆる初心者マークです。どこぞのチュートリアルに載ってたこのコードが通らないので困る。最後の odd k の型が合わないらしい。
あと dotted pattern っていうのもいまいち理解に自信がない。型から値がわかるような仮引数につけるっぽいんだけど、それ以外の用法もあるっぽい？誰か「初めての Agda」(O'Reilly)みたいなのを書いてください。

module Views where
  data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

  _+_ : Nat -> Nat -> Nat
  zero + _ = zero
  (succ m) + n = succ (m + n)
  _*_ : Nat -> Nat -> Nat
  zero * _ = zero
  (succ zero) * n = n
  (succ m) * n = m + (m * n)
  
  one = succ zero
  two = succ one

  data Parity : Nat -> Set where
    even : (k : Nat) -> Parity (k * two)
    odd  : (k : Nat) -> Parity (one + (k * two))

  parity : (n : Nat) -> Parity n
  parity zero = even zero
  parity (succ n) with parity n
  parity (succ .(k * two))         | even k = odd k
  parity (succ .(one + (k * two))) | odd  k = even (succ k)

zero != k * succ (succ zero) of type Nat
when checking that the expression odd k has type
Parity (succ (k * succ (succ zero)))