From ef27c1d191b8d45433b48fff3d89302a7f55253d Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Fri, 7 Sep 2018 12:39:46 +0100 Subject: [PATCH] small updates --- Makefile | 2 +- README.md | 12 ++++++++++++ src/plfa/Acknowledgements.lagda | 1 + src/plfa/Connectives.lagda | 2 +- src/plfa/Induction.lagda | 1 - src/plfa/Naturals.lagda | 3 ++- src/plfa/Properties.lagda | 8 ++++---- 7 files changed, 21 insertions(+), 8 deletions(-) diff --git a/Makefile b/Makefile index e6d26c61..f1a7aae8 100644 --- a/Makefile +++ b/Makefile @@ -14,7 +14,7 @@ out/: mkdir -p out/ out/%.md: src/%.lagda | out/ - agda2html --verbose --link-to-agda-stdlib --use-jekyll=out/ -i $< -o $@ 2>&1 \ + agda2html --verbose --link-to-agda-stdlib --local-references --use-jekyll=out/ -i $< -o $@ 2>&1 \ | sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d' @sed -i '1 s|---|---\nsrc : $(<)|' $@ diff --git a/README.md b/README.md index 2a196300..be8e4e30 100644 --- a/README.md +++ b/README.md @@ -32,6 +32,15 @@ The visible page appears at localhost:4000/ + +## Updates to agda2html + +Go to your clone of the agda2html repository, and run + + $ git pull + $ stack install + + ## Unicode abbreviations @@ -46,6 +55,7 @@ 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` ? create hole @@ -56,6 +66,7 @@ for more details. See [the emacs-mode docs](http://agda.readthedocs.io/en/latest/tools/emacs-mode.html) for more details. + ## Markdown For an overview of the Markdown syntax, see @@ -85,6 +96,7 @@ You can check this worked: nothing added to commit but untracked files present (use "git add" to track) bruichladdich$ + ## Analytics [Google Analytics](http://analytics.google.com/analytics/web/) diff --git a/src/plfa/Acknowledgements.lagda b/src/plfa/Acknowledgements.lagda index a121f682..8c370e5e 100644 --- a/src/plfa/Acknowledgements.lagda +++ b/src/plfa/Acknowledgements.lagda @@ -29,6 +29,7 @@ For pull requests: * Léo Gillot-Lamure * Zbigniew Stanasiuk * Anish Tondwalkar +* Spencer Whitt For answering questions on the Agda mailing list: * Guillaume Allais diff --git a/src/plfa/Connectives.lagda b/src/plfa/Connectives.lagda index 0803bfc0..e5dd6a82 100644 --- a/src/plfa/Connectives.lagda +++ b/src/plfa/Connectives.lagda @@ -1,7 +1,7 @@ --- title : "Connectives: Conjunction, disjunction, and implication" layout : page -prev : /Isomorphisms/ +prev : /Isomorphism/ permalink : /Connectives/ next : /Negation/ --- diff --git a/src/plfa/Induction.lagda b/src/plfa/Induction.lagda index b48142c3..bac229c6 100644 --- a/src/plfa/Induction.lagda +++ b/src/plfa/Induction.lagda @@ -586,7 +586,6 @@ Write out what is known about associativity of addition on each of the first fou days using a finite story of creation, as [earlier]({{ site.baseurl }}{% link out/plfa/Naturals.md %}#finite-creation). - ## Associativity with rewrite There is more than one way to skin a cat. Here is a second proof of diff --git a/src/plfa/Naturals.lagda b/src/plfa/Naturals.lagda index dd2066e6..1f735f8d 100644 --- a/src/plfa/Naturals.lagda +++ b/src/plfa/Naturals.lagda @@ -603,8 +603,9 @@ the 1920's. I was told a joke: "It should be called schönfinkeling, but currying is tastier". Only later did I learn that the explanation of the misattribution was itself a misattribution. The idea actually appears in the _Begriffschrift_ of Gottlob Frege, published in 1879. + ## The story of creation, revisited diff --git a/src/plfa/Properties.lagda b/src/plfa/Properties.lagda index 075eb6e1..9456d021 100644 --- a/src/plfa/Properties.lagda +++ b/src/plfa/Properties.lagda @@ -1441,11 +1441,11 @@ false, give a counterexample. Suppose instead that we add a new term `foo` with the following reduction rules: - ------------------ β-foo₁ - (λ x ⇒ ` x) —→ foo + ------------------ β-foo₁ + (λ x ⇒ ` x) —→ foo - ----------- β-foo₂ - foo —→ zero + ----------- β-foo₂ + foo —→ zero Which of the following properties remain true in the presence of this rule? For each one, write either