From 6ff8e77c221b6186e2785bf27f1a0251066852a1 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Wed, 13 Sep 2017 17:34:32 +0100 Subject: [PATCH] changes to README and config --- README.md | 21 ++++++++------------- _config.yml | 4 ++-- src/Stlc.lagda | 3 +++ 3 files changed, 13 insertions(+), 15 deletions(-) diff --git a/README.md b/README.md index 8b452fef..1dd415d6 100644 --- a/README.md +++ b/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/ -## 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 +). + diff --git a/_config.yml b/_config.yml index 114d4b8f..82910942 100644 --- a/_config.yml +++ b/_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. diff --git a/src/Stlc.lagda b/src/Stlc.lagda index fae038d7..35f314b1 100644 --- a/src/Stlc.lagda +++ b/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.