From 5f4c23d3864249d39a5e8c70b44e679e269a92a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Thu, 27 Jun 2019 17:05:09 +0200 Subject: [PATCH 1/3] Properties: adds a full stop at the end of a sentence --- src/plfa/Properties.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/Properties.lagda b/src/plfa/Properties.lagda index f5736580..29e86e19 100644 --- a/src/plfa/Properties.lagda +++ b/src/plfa/Properties.lagda @@ -498,7 +498,7 @@ the variable appears in `Δ`. * If the term is a lambda abstraction, use the previous lemma to extend the map `ρ` suitably and use induction to rename the body of the -abstraction +abstraction. * If the term is an application, use induction to rename both the function and the argument. From 8deac3076636ba5464af34086cbb01e5b6d3e6e8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Thu, 27 Jun 2019 17:36:27 +0200 Subject: [PATCH 2/3] Properties: changes the indentation of the rename function's signature --- src/plfa/Properties.lagda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/plfa/Properties.lagda b/src/plfa/Properties.lagda index f5736580..259c423c 100644 --- a/src/plfa/Properties.lagda +++ b/src/plfa/Properties.lagda @@ -476,9 +476,9 @@ With the extension lemma under our belts, it is straightforward to prove renaming preserves types: \begin{code} rename : ∀ {Γ Δ} - → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) - ---------------------------------- - → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) + → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) + ---------------------------------- + → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) rename ρ (⊢` ∋w) = ⊢` (ρ ∋w) rename ρ (⊢ƛ ⊢N) = ⊢ƛ (rename (ext ρ) ⊢N) rename ρ (⊢L · ⊢M) = (rename ρ ⊢L) · (rename ρ ⊢M) From 8754f5c9c6f5c671e8865354ec21832f11b7e953 Mon Sep 17 00:00:00 2001 From: Fangyi Zhou Date: Sun, 30 Jun 2019 18:13:02 +0100 Subject: [PATCH 3/3] Lists: Fix a typo in Monoids --- 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 032d3808..ab3ba153 100644 --- a/src/plfa/Lists.lagda +++ b/src/plfa/Lists.lagda @@ -696,7 +696,7 @@ postulate ## Monoids Typically when we use a fold the operator is associative and the -value is a left and right identity for the value, meaning that the +value is a left and right identity for the operator, meaning that the operator and the value form a _monoid_. We can define a monoid as a suitable record type: