agda-unused-0.2.0: data/declaration/Mutual1.agda

module Mutual1 where

data Bool
  : Set
  where

  false
    : Bool

  true
    : Bool

data ℕ
  : Set
  where

  zero
    : ℕ

  suc
    : ℕ
    → ℕ

is-even
  : ℕ
  → Bool

is-odd
  : ℕ
  → Bool

is-even zero
  = true
is-even (suc n)
  = is-odd n

is-odd zero
  = false
is-odd (suc n)
  = is-even n