Data hosted with ♥ by Pastebin.com - Download Raw - See Original
  1. type family GCD d m n
  2. type instance GCD d Zero Zero = d
  3. type instance GCD d (Succ m) (Succ n) = GCD (Succ d) m n
  4. type instance GCD Zero (Succ m) Zero = Succ m
  5. type instance GCD (Succ d) (Succ m) Zero = GCD (Succ Zero) d m
  6. type instance GCD Zero Zero (Succ n) = Succ n
  7. type instance GCD (Succ d) Zero (Succ n) = GCD (Succ Zero) d n