From cb173780f56ad396c581d4dd3be4cda2f085b4e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bjo=CC=88rn=20Buckwalter?= <bjorn@buckwalter.se>
Date: Fri, 10 Feb 2012 12:01:00 +0800
Subject: [PATCH] Simplified DivP instance, now with derivation.

---
 Numeric/NumType/TF.lhs | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Numeric/NumType/TF.lhs b/Numeric/NumType/TF.lhs
index 338e57e..8a25509 100644
--- a/Numeric/NumType/TF.lhs
+++ b/Numeric/NumType/TF.lhs
@@ -243,12 +243,14 @@ necessary to ensure bad division terminates with a proper error
 instead of overflowing the context stack (more confusing).
 
 > type family DivP n m            -- n / m.
-> type instance DivP Z (S n) = Z  -- Trivially.
 
-The recursive instance for division is quite complex and in fact I
-do not recall how I derived it. But it works (I promise!).
+The instances for division is based on the identities:
+
+    0 / y = 0,               for y >= 1.
+    x / y = (x - y) / y + 1, for x >= y >= 1.
 
-> type instance DivP (S n) (S n') = S (DivP (Pred (Sub (S n) n')) (S n'))  -- Oh my!
+> type instance DivP Z (S n) = Z  -- Trivially.
+> type instance DivP (S n) (S m) = S (DivP (Sub (S n) (S m)) (S m))  -- Oh my!
 
 Now we can generalize division to negative numbers too, building on
 top of 'DivP'. A trivial but tedious exercise.