From c8ca573d8a6432b6d116bff845462ae95fff212c Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Fri, 4 May 2018 15:05:55 -0300
Subject: [PATCH] fixed alpha renaming example in Stlc

---
 src/FreshUnstuck.lagda | 2 +-
 src/Stlc.lagda         | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/FreshUnstuck.lagda b/src/FreshUnstuck.lagda
index 4f049459..3be74327 100644
--- a/src/FreshUnstuck.lagda
+++ b/src/FreshUnstuck.lagda
@@ -1,7 +1,7 @@
 ---
 title     : "FreshUnstuck: Generation of fresh names with strings"
 layout    : page
-permalink : /TypedFresh
+permalink : /FreshUnstuck
 ---
 
 Generation of fresh names, where names are string-integer pairs.
diff --git a/src/Stlc.lagda b/src/Stlc.lagda
index 0b704e4d..a9ab7c5c 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -121,8 +121,8 @@ We use the following special characters
 
     ⇒  U+21D2: RIGHTWARDS DOUBLE ARROW (\=>)
     `  U+0060: GRAVE ACCENT 
-    λ  U+03BB:  GREEK SMALL LETTER LAMBDA (\Gl or \lambda)
-    ∶  U+2236:  RATIO (\:)
+    λ  U+03BB: GREEK SMALL LETTER LAMBDA (\Gl or \lambda)
+    ∶  U+2236: RATIO (\:)
     ·  U+00B7: MIDDLE DOT (\cdot)
 
 Note that ∶ (U+2236 RATIO) is not the same as : (U+003A COLON).
@@ -183,7 +183,7 @@ irrelevant.  Thus the five terms
 * `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) ``
 * `` λ[ g ∶ 𝔹 ⇒ 𝔹 ] λ[ y ∶ 𝔹 ] ` g · (` g · ` y) ``
 * `` λ[ fred ∶ 𝔹 ⇒ 𝔹 ] λ[ xander ∶ 𝔹 ] ` fred · (` fred · ` xander) ``
-* `` λ[ 😈 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😄 ∶ 𝔹 ] ` 😈 · (` 😈 · ` 😄) ``  
+* `` λ[ 😇 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😈  ∶ 𝔹 ] ` 😇 · (` 😇 · ` 😈 ) ``  
 * `` λ[ x ∶ 𝔹 ⇒ 𝔹 ] λ[ f ∶ 𝔹 ] ` x · (` x · ` f) ``
 
 are all considered equivalent.  This equivalence relation
@@ -227,8 +227,8 @@ same names.
 
 #### Special characters
 
+    😇  U+1F607: SMILING FACE WITH HALO
     😈  U+1F608: SMILING FACE WITH HORNS
-    😄  U+1F604: SMILING FACE WITH OPEN MOUTH AND SMILING EYES
 
 #### Precedence