Haskell doodle made while reading about Twelf.

Twelf.hs

-- Haskell doodle made while reading about Twelf.
-- http://twelf.org/wiki/Proving_metatheorems_with_Twelf

module Twelf where

data Nat
  = Zero
  | Succ Nat
  deriving (Eq, Show)

class Even a where
  isEven :: a -> Bool

instance Even Nat where
  isEven Zero            = True
  isEven (Succ (Succ x)) = isEven x
  isEven _               = False

class Plus a where
  plus :: a -> a -> a -> Bool

instance Plus Nat where
  plus Zero     y z        = y == z
  plus (Succ x) y (Succ z) = plus x y z

one   = Succ Zero
two   = Succ one
three = Succ two
four  = Succ three
five  = Succ four