changes to README and config

README.md

@@ -15,13 +15,14 @@ and
 [Philip Wadler](
 http://homepages.inf.ed.ac.uk/wadler/
 ).
+Please send us comments! Contact details below.
 
 
 ## How to host literate code
 
 In directory `sf/` run the following:
 
-	$ make clobber
+    $ make clobber
     $ make
     $ make serve &
 
@@ -29,18 +30,6 @@ The visible page appears at
 
     localhost:4000/sf/<permalink>
 
-## Markdown
-
-For markdown commands see [Daring Fireball](
-https://daringfireball.net/projects/markdown/syntax
-).
-
-## Important git commands
-
-    git pull
-    git commit -am "message"
-    git push
-
 ## Unicode abbreviations
 
 
@@ -68,3 +57,9 @@ Also see [here](
 http://agda.readthedocs.io/en/latest/tools/emacs-mode.html
 ).
 
+## Markdown
+
+For markdown commands see [Daring Fireball](
+https://daringfireball.net/projects/markdown/syntax
+).
+

_config.yml

@@ -8,10 +8,10 @@ author: Wen Kokke
 contributors:
   - name: Wen Kokke
     email: wen.kokke@ed.ac.uk
-    github_username: wenkokke
+    twitter_username: wenkokke
   - name: Philip Wadler
     email: wadler@inf.ed.ac.uk
-    github_username: wadler
+    twitter_username: philipwadler
 
 description: > 
   Software Foundations in Agda.

src/Stlc.lagda

@@ -192,6 +192,9 @@ is sometimes called _alpha renaming_.
 As we descend from a term into its subterms, variables
 that are bound may become free.  Consider the following terms.
 
+
+
+
 * `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) ``
   Both variable `f` and `x` are bound.