From a5e1f77d22b9e7f13163e3d03fc6b9f1ff6d5e75 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Wed, 25 Aug 2021 11:53:30 +0100
Subject: [PATCH] Changed header anchors. Commited WIP fix for #577.

---
 book/lua/single-file-identifiers.lua | 31 ++++++++++++++++++++++++++++
 src/plfa/part2/Subtyping.lagda.md    |  4 ++--
 2 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 book/lua/single-file-identifiers.lua

diff --git a/book/lua/single-file-identifiers.lua b/book/lua/single-file-identifiers.lua
new file mode 100644
index 00000000..9ea3e7a7
--- /dev/null
+++ b/book/lua/single-file-identifiers.lua
@@ -0,0 +1,31 @@
+local chapter = nil
+
+function Header(el)
+  if el.level == 2 then
+    chapter = el.attr.identifier
+  end
+  if el.level >= 3 then
+    if el.attr.attributes.name then
+      el.attr.identifier = chapter .. '-' .. el.attr.attributes.name
+      el.attr.attributes.name = nil
+    else
+      el.attr.identifier = chapter .. '-' .. el.attr.identifier
+    end
+  end
+end
+
+function show(t)
+  local str = ''
+  str = str .. '{'
+  for k,v in pairs(t) do
+    str = str .. k
+    str = str .. ':'
+    if type(v) == 'table' then
+      str = str .. show(v)
+    else
+      str = str .. v
+    end
+  end
+  str = str .. '}'
+  return str
+end
diff --git a/src/plfa/part2/Subtyping.lagda.md b/src/plfa/part2/Subtyping.lagda.md
index 71836424..73a4cd49 100644
--- a/src/plfa/part2/Subtyping.lagda.md
+++ b/src/plfa/part2/Subtyping.lagda.md
@@ -879,7 +879,7 @@ typed (C-suc c) = ⊢suc (typed c)
 typed (C-rcd ⊢Ms dks As<:Bs) = ⊢<: (⊢rcd ⊢Ms dks) As<:Bs
 ```
 
-## Progress <a #"subtyping-progress"></a>
+## Progress {#subtyping-progress}
 
 The Progress theorem states that a well-typed term may either take a
 reduction step or it is already a value. The proof of Progress is like
@@ -952,7 +952,7 @@ progress (⊢<: {A = A}{B} ⊢M A<:B)           =  progress ⊢M
 * Case `⊢<:`: we invoke the induction hypothesis on sub-derivation of `Γ ⊢ M ⦂ A`.
 
 
-## Preservation <a #"subtyping-preservation"></a>
+## Preservation {#subtyping-preservation}
 
 In this section we prove that when a well-typed term takes a reduction
 step, the result is another well-typed term with the same type.