Mutually defined indexed datatypes Even and Odd

Even.agda

module Even where

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

-- Declare _Odd datatype first
-- is to be used by _Even datatype
data _Odd : ℕ → Set

-- Declare and define _Even
data _Even : ℕ → Set where
  0-is-even : _Even 0
  suc_is-even-if : (n : ℕ) → _Odd n → _Even (suc n)

-- Define _Odd
data _Odd where
  suc_is-odd-if : (n : ℕ) → _Even n → _Odd (suc n)