diff --git a/hs/agda-count b/hs/agda-count
new file mode 100755
index 00000000..d17f98f7
Binary files /dev/null and b/hs/agda-count differ
diff --git a/hs/agda-count.hs b/hs/agda-count.hs
index eaf806ad..f6136b6b 100644
--- a/hs/agda-count.hs
+++ b/hs/agda-count.hs
@@ -1,11 +1,5 @@
 import Prelude
 
-begin :: String
-begin =  "\\begin{code}"
-
-end :: String
-end =  "\\end{code}"
-
 prefix :: Eq a => [a] -> [a] -> Bool
 prefix xs ys  =  take (length xs) ys == xs
 
@@ -33,11 +27,19 @@ count b e = sum . map length . strip b e
 test2 :: Bool
 test2 =  count (== 'b') (== 'e') ex1 == 6
 
-info :: String -> IO (Int , Int)
-info f =
-  do xs <- readFile f
-     return ((length . lines) xs),
-             (count (prefix begin) (prefix end) . lines) xs)
+agda :: String -> Int
+agda =  count (prefix begin) (prefix end) . lines
+  where
+  begin  =  "\\begin{code}"
+  end    =  "\\end{code}"
+
+wc :: String -> Int
+wc =  length . lines
+
+type Name = String
+
+info :: String -> (Int, Int)
+info xs = (wc xs, agda xs)
 
 pad :: Int -> String -> String
 pad n s  =  take n (s ++ repeat ' ')
@@ -45,21 +47,30 @@ pad n s  =  take n (s ++ repeat ' ')
 rjust :: Int -> String -> String
 rjust n = reverse . pad n . reverse
 
-format :: String -> IO String
-format "--" = ""
-format f =
-  do (lines, code) <- info f
-     return (replicate 4 ' ' ++
-             pad 28 f ++
-             rjust 4 lines ++
-             replicate 4 ' ' ++
-             rjust 4 ' ')
+format :: Name -> (Int, Int) -> String
+format name (wc, ag) =
+  (replicate 4 ' ' ++
+   pad 28 name ++
+   rjust 4 (show wc) ++
+   replicate 4 ' ' ++
+   rjust 4 (show ag))
 
-config : IO [String]
-config =
-  do stuff <- readFile "config.txt"
-     return (lines stuff)
+process :: Name -> IO String
+process "--"  =  return ""
+process name  =
+  do xs <- readFile (pre ++ name ++ post)
+     return (format name (info xs))
+  where
+  pre  = "../src/plta/"
+  post = ".lagda"
 
-answer : IO String
-answer =
-  do 
\ No newline at end of file
+header :: String
+header =
+  unlines
+    ["                                total   code",
+     "                                -----   ----"]
+main :: IO ()
+main =
+  do config <- readFile "config.txt"
+     content <- sequence (map process (lines config))
+     putStrLn (header ++ unlines content)
diff --git a/hs/config.txt b/hs/config.txt
new file mode 100644
index 00000000..195ab4a8
--- /dev/null
+++ b/hs/config.txt
@@ -0,0 +1,23 @@
+Preface
+--
+Naturals
+Properties
+Relations
+Equality
+Isomorphism
+Connectives
+Negation
+Quantifiers
+Lists
+Decidable
+--
+Lambda
+Properties
+DeBruijn
+Extensions
+Inference
+Untyped
+--
+Acknowledgements
+Fonts
+Statistics
diff --git a/src/plta/DeBruijn.lagda b/src/plta/DeBruijn.lagda
index dfa45cd8..15f533c7 100644
--- a/src/plta/DeBruijn.lagda
+++ b/src/plta/DeBruijn.lagda
@@ -330,13 +330,13 @@ judgements:
 * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "s" ⦂ `ℕ ⇒ `ℕ ``
 
 They correspond to the following inherently-typed variables.
-\begin{code}
+-- \begin{code}
 _ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ
 _ = Z
 
 _ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ ⇒ `ℕ
 _ = S Z
-\end{code}
+-- \end{code}
 In the given context, `"z"` is represented by `Z`, and `"s"` by `S Z`.
 
 ### Terms and the typing judgement
@@ -1348,4 +1348,16 @@ tedious and almost identical to the previous proof.
 
 Counting the lines of code is instructive.  While this chapter
 covers the same formal development as the previous two
-chapters, it has about half the number of lines of code.
+chapters, it has much less code.  Omitting all the examples,
+and all proofs that appear in Properties but not DeBruijn
+(such as the proof that reduction is deterministic), the
+number of lines of code is as follows.
+
+    Lambda                      216
+    Properties                  235
+    DeBruijn                    275
+
+The relation between the two approaches approximates the
+golden ratio: raw terms with a separate typing relation
+require about 1.6 times as much code as inherently-typed terms
+with de Bruijn indices.
diff --git a/src/plta/Properties.lagda b/src/plta/Properties.lagda
index cf889d69..fd35c10e 100644
--- a/src/plta/Properties.lagda
+++ b/src/plta/Properties.lagda
@@ -1369,7 +1369,7 @@ det β-zero        β-zero            =  refl
 det (β-suc VL)    (ξ-case L—→L″)    =  ⊥-elim (V¬—→ (V-suc VL) L—→L″)
 det (β-suc _)     (β-suc _)         =  refl
 det β-μ           β-μ               =  refl
-\end{code}
+-- \end{code}
 The proof is by induction over possible reductions.  We consider
 three typical cases.
 
diff --git a/src/plta/Statistics.lagda b/src/plta/Statistics.lagda
index 734e1e61..d73561a4 100644
--- a/src/plta/Statistics.lagda
+++ b/src/plta/Statistics.lagda
@@ -9,29 +9,30 @@ module plta.Statistics where
 \end{code}
 
 Total number of lines and number of lines of Agda code in each chapter
-(as of 11 June 2018).
+(as of 2 July 2018).
 
                                 total   code
-    Preface                       94       1
+                                -----   ----
+    Preface                       99       1
 
     Naturals                     900      86
-    Properties                   766     107
-    Relations                    608      93    
-    Equality                     669     141
-    Isomorphism                  310     153
-    Connectives                  826     245
+    Properties                  1533     724
+    Relations                    608      93
+    Equality                     595     128
+    Isomorphism                  403     170
+    Connectives                  827     243
     Negation                     354      47
-    Quantifiers                  399      82
-    Lists                        901     414
+    Quantifiers                  390      79
+    Lists                        893     412
     Decidable                    566     170
 
-    Lambda                      1114     345
-    Properties                   827     450
-    DeBruijn                     477     351
+    Lambda                      1300     386
+    Properties                  1533     724
+    DeBruijn                    1363     627
     Extensions                   603     524
-    Inference                    428     350
-    Untyped                      346     265
+    Inference                    431     350
+    Untyped                      362     281
 
     Acknowledgements              46       1
-    Fonts                         61      23
-    Statistics                    34       1
+    Fonts                         62      44
+    Statistics                    38       1