Issue162.agda

-- Now you don't need a mutual keyword anymore!
module Issue162 where

data Odd : Set
data Even : Set where
  zero : Even
  suc  : Odd → Even

data Odd where
  suc : Even → Odd

-- This means you can have all kinds of things in
-- mutual blocks.

-- Like postulates
_o+e_ : Odd → Even → Odd

_e+e_ : Even → Even → Even
zero e+e m = m
suc n e+e m = suc (n o+e m)

postulate todo : Even

suc n o+e m = suc todo

-- Or modules
_e+o_ : Even → Odd → Odd
_o+o_ : Odd → Odd → Even
suc n o+o m = suc (n e+o m)

module Helper where
  f : Even → Odd → Odd
  f zero    m = m
  f (suc n) m = suc (n o+o m)

n e+o m = Helper.f n m

-- Multiplication just for the sake of it
_o*o_ : Odd → Odd → Odd
_e*o_ : Even → Odd → Even
zero  e*o m = zero
suc n e*o m = m o+o (n o*o m)

suc n o*o m = m o+e (n e*o m)