power.agda

data Parity : ℕ -> Set where
  even : (k : ℕ) -> Parity (k * 2)
  odd  : (k : ℕ) -> Parity (1 + k * 2)

parity : (n : ℕ) -> Parity n
parity zero = even zero
parity (succ n) with parity n
parity (succ .(k * 2)) | even k = odd k
parity (succ .(1 + k * 2)) | odd k = even (succ k)

power : ℕ -> ℕ -> ℕ
power m zero = 1
power m (succ n) with parity n
power m (succ .(k * 2)) | even k = power (m * m) k
power m (succ .(1 + k * 2)) | odd k = m * (power (m * m) k)