From 799d924e8b79fdae3837f6bffcde30f4921d4ce7 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Tue, 4 Sep 2018 19:34:32 +0100 Subject: [PATCH] small fixes --- Notes.md | 6 ++++++ README.md | 45 ++++++++++++++++++++++++++++------------ src/plfa/Inference.lagda | 26 +++++++++++------------ 3 files changed, 51 insertions(+), 26 deletions(-) diff --git a/Notes.md b/Notes.md index 968f8484..3b349aab 100644 --- a/Notes.md +++ b/Notes.md @@ -1,5 +1,11 @@ # Notes +> We want to alert you that you've been granted the following access: +> Manage Users and Edit +> to the Google Analytics account `plfa (UA-125055580)` by `wen.kokke@gmail.com`. + +> [Google analytics](http://analytics.google.com/analytics/web/) + ## Where to put Lists? Three possible orders: diff --git a/README.md b/README.md index baae3dfe..65093869 100644 --- a/README.md +++ b/README.md @@ -4,11 +4,18 @@ title: About permalink: /about/ --- -This book is an introduction to programming language theory, written in Agda. The authors are [Wen Kokke](https://twitter.com/wenkokke) and [Philip Wadler](https://softwarefoundations.cis.upenn.edu/). +This book is an introduction to programming language theory, written +in Agda. The authors are [Wen Kokke](https://twitter.com/wenkokke) +and [Philip Wadler](https://softwarefoundations.cis.upenn.edu/). -Please send us comments! The text is currrently being drafted. The first draft of Part I will be completed before the end of March 2018. When that is done it will be announced here, and that would be an excellent time to comment on the first part. +Please send us comments! The text is currrently being drafted. The +first draft of Part I will be completed before the end of March +2018. When that is done it will be announced here, and that would be +an excellent time to comment on the first part. -The book was inspired by [Software Foundations](https://softwarefoundations.cis.upenn.edu), but presents the material in a different way; see the [Preface](/Preface/). +The book was inspired by [Software +Foundations](https://softwarefoundations.cis.upenn.edu), but presents +the material in a different way; see the [Preface](/Preface/). ## How to host literate code @@ -35,7 +42,9 @@ The visible page appears at x\_1 x₁ x\_i xᵢ -See [agda-input.el](https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194) for more details. +See +[agda-input.el](https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194) +for more details. ## How to use `agda-mode` @@ -49,7 +58,10 @@ See [the emacs-mode docs](http://agda.readthedocs.io/en/latest/tools/emacs-mode. ## Markdown -For an overview of the Markdown syntax, see [the original description](https://daringfireball.net/projects/markdown/syntax), [the CommonMark project](https://spec.commonmark.org/0.28/), or [the version that is used in this book](https://kramdown.gettalong.org/syntax.html). +For an overview of the Markdown syntax, see +[the original description](https://daringfireball.net/projects/markdown/syntax), +[the CommonMark project](https://spec.commonmark.org/0.28/), or +[the version that is used in this book](https://kramdown.gettalong.org/syntax.html). ## Git @@ -61,14 +73,21 @@ Checkout this repository with You can check this worked: bruichladdich$ cd plfa.github.io - bruichladdich$ git status - On branch dev - Your branch is up-to-date with 'origin/dev'. + bruichladdich$ git status + On branch dev + Your branch is up-to-date with 'origin/dev'. - Untracked files: - (use "git add ..." to include in what will be committed) + Untracked files: + (use "git add ..." to include in what will be committed) - out/ + out/ + + nothing added to commit but untracked files present (use "git add" to track) + bruichladdich$ + +## Analytics + +Wen and Phil have permission to view +[Google Analytics](http://analytics.google.com/analytics/web/) +account `plfa (UA-125055580)`. - nothing added to commit but untracked files present (use "git add" to track) - bruichladdich$ diff --git a/src/plfa/Inference.lagda b/src/plfa/Inference.lagda index c9c86ee8..d91a4582 100644 --- a/src/plfa/Inference.lagda +++ b/src/plfa/Inference.lagda @@ -995,16 +995,16 @@ type judgement into the corresponding inherently typed term. First, we give code to erase a context. \begin{code} ∥_∥Γ : Context → DB.Context -∥ ∅ ∥Γ = DB.∅ -∥ Γ , x ⦂ A ∥Γ = ∥ Γ ∥Γ DB., A +∥ ∅ ∥Γ = DB.∅ +∥ Γ , x ⦂ A ∥Γ = ∥ Γ ∥Γ DB., A \end{code} It simply drops the variable names. Next, we give code to erase a lookup judgment. \begin{code} ∥_∥∋ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ∥ Γ ∥Γ DB.∋ A -∥ Z ∥∋ = DB.Z -∥ S x≢ ⊢x ∥∋ = DB.S ∥ ⊢x ∥∋ +∥ Z ∥∋ = DB.Z +∥ S x≢ ⊢x ∥∋ = DB.S ∥ ⊢x ∥∋ \end{code} It just drops the evidence that variable names are distinct. @@ -1015,16 +1015,16 @@ there are two mutually recursive erasure functions. ∥_∥⁺ : ∀ {Γ M A} → Γ ⊢ M ↑ A → ∥ Γ ∥Γ DB.⊢ A ∥_∥⁻ : ∀ {Γ M A} → Γ ⊢ M ↓ A → ∥ Γ ∥Γ DB.⊢ A -∥ ⊢` ⊢x ∥⁺ = DB.` ∥ ⊢x ∥∋ -∥ ⊢L · ⊢M ∥⁺ = ∥ ⊢L ∥⁺ DB.· ∥ ⊢M ∥⁻ -∥ ⊢↓ ⊢M ∥⁺ = ∥ ⊢M ∥⁻ +∥ ⊢` ⊢x ∥⁺ = DB.` ∥ ⊢x ∥∋ +∥ ⊢L · ⊢M ∥⁺ = ∥ ⊢L ∥⁺ DB.· ∥ ⊢M ∥⁻ +∥ ⊢↓ ⊢M ∥⁺ = ∥ ⊢M ∥⁻ -∥ ⊢ƛ ⊢N ∥⁻ = DB.ƛ ∥ ⊢N ∥⁻ -∥ ⊢zero ∥⁻ = DB.`zero -∥ ⊢suc ⊢M ∥⁻ = DB.`suc ∥ ⊢M ∥⁻ -∥ ⊢case ⊢L ⊢M ⊢N ∥⁻ = DB.case ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻ -∥ ⊢μ ⊢M ∥⁻ = DB.μ ∥ ⊢M ∥⁻ -∥ ⊢↑ ⊢M refl ∥⁻ = ∥ ⊢M ∥⁺ +∥ ⊢ƛ ⊢N ∥⁻ = DB.ƛ ∥ ⊢N ∥⁻ +∥ ⊢zero ∥⁻ = DB.`zero +∥ ⊢suc ⊢M ∥⁻ = DB.`suc ∥ ⊢M ∥⁻ +∥ ⊢case ⊢L ⊢M ⊢N ∥⁻ = DB.case ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻ +∥ ⊢μ ⊢M ∥⁻ = DB.μ ∥ ⊢M ∥⁻ +∥ ⊢↑ ⊢M refl ∥⁻ = ∥ ⊢M ∥⁺ \end{code} Erasure replaces constructors for each typing judgement by the corresponding term constructor from `DB`. The