EvenOdd.idr

module EvenOdd

import Data.Fin

%access public export
%default total

data Even : (n: Nat) -> Type where
  ZEven : Even Z
  SsEven : (n: Nat) -> Even n -> Even (S (S n))

data Odd : Nat -> Type where
  OneOdd : Odd 1
  SsOdd : Odd n -> Odd (2 + n)

oddNotZero : Odd 0 -> Void
oddNotZero OneOdd impossible
oddNotZero (SsOdd _) impossible

notOddSs : Not (Odd n) -> Not (Odd (2 + n))
notOddSs a b = case b of
  (SsOdd x) => ?notOddSs_rhs_2

evenNotOdd : Even n -> Not (Odd n)
evenNotOdd ZEven = oddNotZero
evenNotOdd (SsEven n x) =
  let rec = evenNotOdd x
  in notOddSs rec