div.hs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, TypeOperators #-}
module Main where
import GHC.TypeLits

type family Div2 (n :: Nat) where
  Div2 0 = 0
  Div2 1 = 0
  Div2 n = Div2 (n - 2) + 1

type family Div2 (n :: Nat) where
  Div2 0 = 0
  Div2 1 = 0
  Div2 n = Div2 (n - 2) + 1

type family If (p :: Bool) (t :: k) (f :: k) where
  If True  a b = a
  If False a b = b

type family n < m where
  0 < 0 = False
  0 < n = True
  n < 0 = False
  m < n = (m - 1) < (n - 1)

type family n / m where
  n / 0 = 0
  0 / k = 0
  n / n = 1
  n / k = If (n < k) 0 (((n - k) / k) + 1)