Idris code from Sydney Type Theory meeting 5 June 2017

EvenOdd.idr

module EvenOdd

data Even : (n : Nat) -> Type where
  ZeroIsEven   : Even 0
  SuccSuccEven : Even n -> Even (S (S n))

data Odd : (n : Nat) -> Type where
  OneIsOdd    : Odd 1
  SuccSuccOdd : Odd n -> Odd (S (S n))


total
evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)
evenOrOdd Z         = Left ZeroIsEven
evenOrOdd (S Z)     = Right OneIsOdd
evenOrOdd (S (S k)) = case evenOrOdd k of
                           Left l  => Left (SuccSuccEven l)
                           Right r => Right (SuccSuccOdd r)

thereExistsAnOddNatural : (n : Nat ** Odd n)
thereExistsAnOddNatural = (5 ** (SuccSuccOdd (SuccSuccOdd OneIsOdd)))

--------------------------------------------------------------------------------

mutual
  data Even' : (n : Nat) -> Type where
    ZeroEven : Even' 0
    SuccOdd  : Odd' n -> Even' (S n)

  data Odd' : (n : Nat) -> Type where
    SuccEven : Even' n -> Odd' (S n)

total
f : (n : Nat) -> Either (Even' n) (Odd' n) -> Either (Even' (S n)) (Odd' (S n))
f Z (Left ZeroEven)        = Right (SuccEven ZeroEven)
f (S k) (Left (SuccOdd x)) = Right (SuccEven (SuccOdd x))
f (S n) (Right r)          = Left (SuccOdd r)