small fixes
This commit is contained in:
Philip Wadler
parent
94e5da0236
commit
799d924e8b
3 changed files with 51 additions and 26 deletions
6
Notes.md
6
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:
|
||||
|
|
|
|||
45
README.md
45
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 <file>..." to include in what will be committed)
|
||||
Untracked files:
|
||||
(use "git add <file>..." 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$
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue