From 4896989ba2d1ba7f16b1514aa41998f7e7221af1 Mon Sep 17 00:00:00 2001 From: wadler Date: Fri, 11 Jan 2019 09:10:56 +0000 Subject: [PATCH 1/6] Setting up extrinsic branch --- Notes.md | 15 +++++++++++++++ README.md | 3 ++- 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/Notes.md b/Notes.md index d2d46e18..768b0c70 100644 --- a/Notes.md +++ b/Notes.md @@ -8,6 +8,21 @@ permalink: /Notes/ +## Git commands + +Git commands to create a branch and pull request + + git help -- get help on + git branch -- list all branches + git branch -- create new local branch + git checkout -- make the current branch + git merge -- merge branch into current branch + git push origin -- make local branch into remote + git rebase -- merge branch into current branch + +On website, use pulldown menu to swith branch and then +click "new pull request" button. + ## Suggestion from Conor for Inference Conor McBride diff --git a/README.md b/README.md index 758dc0dd..40cbaec9 100644 --- a/README.md +++ b/README.md @@ -171,7 +171,8 @@ configuration file at `~/.emacs`, if you have the mentioned fonts available: ## Markdown -The book is written in [Kramdown Markdown](https://kramdown.gettalong.org/syntax.html). +The book is written in +[Kramdown Markdown](https://kramdown.gettalong.org/syntax.html). ## Travis Continuous Integration From 817a9f7de5ae6dc94842f12843cece11ed56eed6 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Fri, 11 Jan 2019 12:24:19 +0000 Subject: [PATCH 2/6] Update Notes.md --- Notes.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Notes.md b/Notes.md index 768b0c70..6aa1d185 100644 --- a/Notes.md +++ b/Notes.md @@ -12,11 +12,11 @@ permalink: /Notes/ Git commands to create a branch and pull request - git help -- get help on + git help -- get help on git branch -- list all branches - git branch -- create new local branch - git checkout -- make the current branch - git merge -- merge branch into current branch + git branch -- create new local branch + git checkout -- make the current branch + git merge -- merge branch into current branch git push origin -- make local branch into remote git rebase -- merge branch into current branch From 88b177f977ae005c3f7aa4e45158478bd40ffc64 Mon Sep 17 00:00:00 2001 From: Yasuhiko Watanabe Date: Sat, 12 Jan 2019 10:08:47 +0900 Subject: [PATCH 3/6] Typo. --- src/plfa/Lists.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/Lists.lagda b/src/plfa/Lists.lagda index e9d3345e..2016188e 100644 --- a/src/plfa/Lists.lagda +++ b/src/plfa/Lists.lagda @@ -778,7 +778,7 @@ operations associate to the left rather than the right. For example: #### Exercise `foldr-monoid-foldl` -Show that if `_⊕_` and `e` form a monoid, then `foldr _⊗_ e` and +Show that if `_⊗_` and `e` form a monoid, then `foldr _⊗_ e` and `foldl _⊗_ e` always compute the same result. From 8a6d9a333796165568818387b8d0210525f13c0c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sat, 12 Jan 2019 11:16:33 +0100 Subject: [PATCH 4/6] Equality chapter: fixes spelling of a word --- src/plfa/Equality.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/Equality.lagda b/src/plfa/Equality.lagda index 533f3a84..2bde4504 100644 --- a/src/plfa/Equality.lagda +++ b/src/plfa/Equality.lagda @@ -348,7 +348,7 @@ an order that will make sense to the reader. The proof of monotonicity from Chapter [Relations][plfa.Relations] -can be written in a more readable form by using an anologue of our +can be written in a more readable form by using an analogue of our notation for `≡-reasoning`. Define `≤-reasoning` analogously, and use it to write out an alternative proof that addition is monotonic with regard to inequality. Rewrite both `+-monoˡ-≤` and `+-mono-≤`. From 8c3ed3b38a67ee2f4ad37326a9ff111664721ffb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sat, 12 Jan 2019 17:43:01 +0100 Subject: [PATCH 5/6] Equality chapter: fixes a recursive call to the intended addition commutativity --- src/plfa/Equality.lagda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/Equality.lagda b/src/plfa/Equality.lagda index 2bde4504..4e04701c 100644 --- a/src/plfa/Equality.lagda +++ b/src/plfa/Equality.lagda @@ -452,8 +452,8 @@ here is a second proof that addition is commutative, relying on rewrites rather than chains of equalities: \begin{code} +-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m -+-comm′ zero n rewrite +-identity n = refl -+-comm′ (suc m) n rewrite +-suc n m | +-comm m n = refl ++-comm′ zero n rewrite +-identity n = refl ++-comm′ (suc m) n rewrite +-suc n m | +-comm′ m n = refl \end{code} This is far more compact. Among other things, whereas the previous proof required `cong suc (+-comm m n)` as the justification to invoke From 434b8f5be5812e69526d23414f89c6582b7bebf4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sat, 12 Jan 2019 14:29:39 +0100 Subject: [PATCH 6/6] Equality chapter: removes a redundant verb --- src/plfa/Equality.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/Equality.lagda b/src/plfa/Equality.lagda index 4e04701c..6566f3b9 100644 --- a/src/plfa/Equality.lagda +++ b/src/plfa/Equality.lagda @@ -399,7 +399,7 @@ even-comm : ∀ (m n : ℕ) even-comm m n ev rewrite +-comm n m = ev \end{code} Here `ev` ranges over evidence that `even (m + n)` holds, and we show -that it is also provides evidence that `even (n + m)` holds. In +that it also provides evidence that `even (n + m)` holds. In general, the keyword `rewrite` is followed by evidence of an equality, and that equality is used to rewrite the type of the goal and of any variable in scope.