Merge branch 'dev' into devcontainer

.github/workflows/ci.yml

@@ -214,7 +214,7 @@ jobs:
         shell: pwsh
 
       - name: Create GitHub Release
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
         with:
           files: Website.zip
           body_path: ${{ github.workspace }}/release-notes-${{ steps.setup-bumpver.outputs.current-version }}.md

.pre-commit-config.yaml

@@ -1,6 +1,6 @@
 repos:
 -   repo: https://github.com/pre-commit/pre-commit-hooks
-    rev: v4.5.0
+    rev: v4.6.0
     hooks:
     -   id: check-added-large-files
     -   id: check-case-conflict

package.json

@@ -3,6 +3,6 @@
     "browser-sync": "^3.0.2",
     "html-validate": "^8.11.1",
     "html-minifier": "^4.0.0",
-    "sass": "^1.71.1"
+    "sass": "^1.75.0"
   }
 }

src/plfa/part3/Compositional.lagda.md

@@ -257,7 +257,7 @@ We proceed by induction on the semantics.
       `v′ → v ⊑ v′ → v₁`.
 
 
-The forward direction is proved by cases on the premise `(ℰ L ● ℰ M) γ v`.
+The backward direction is proved by cases on the premise `(ℰ L ● ℰ M) γ v`.
 In case `v ⊑ ⊥`, we obtain `Γ ⊢ L · M ↓ ⊥` by rule `⊥-intro`.
 Otherwise, we conclude immediately by rule `↦-elim`.
 

src/plfa/part3/Soundness.lagda.md

@@ -234,7 +234,7 @@ about `M` and can therefore use `⊥` for the value of `M`.
 
 Previously we showed that renaming variables preserves meaning.  Now
 we prove the opposite, that it reflects meaning. That is,
-if `δ ⊢ rename ρ M ↓ v`, then `γ ⊢ M ↓ v`, where `(δ ∘ ρ) `⊑ γ`.
+if `δ ⊢ rename ρ M ↓ v`, then `γ ⊢ M ↓ v`, where ``(δ ∘ ρ) `⊑ γ``.
 
 First, we need a variant of a lemma given earlier.
 ```agda
@@ -355,7 +355,7 @@ same-const-env : ∀{Γ} {x : Γ ∋ ★} {v} → (const-env x v) x ≡ v
 same-const-env {x = x} rewrite var≟-refl x = refl
 ```
 
-and `const-env x v` maps `y` to `⊥, so long as `x ≢ y`.
+and `const-env x v` maps `y` to `⊥`, so long as `x ≢ y`.
 
 ```agda
 diff-const-env : ∀{Γ} {x y : Γ ∋ ★} {v}
@@ -378,7 +378,7 @@ Now to finish the two cases of the proof.
 
 * In the case where `x ≡ y`, we need to show
   that `γ ⊢ σ y ↓ v`, but that's just our premise.
-* In the case where `x ≢ y,` we need to show
+* In the case where `x ≢ y`, we need to show
   that `γ ⊢ σ y ↓ ⊥`, which we do via rule `⊥-intro`.
 
 Thus, we have completed the variable case of the proof that
@@ -500,7 +500,7 @@ subst-reflect (sub d lt) eq
 ... | ⟨ δ , ⟨ subst-δ , m ⟩ ⟩ = ⟨ δ , ⟨ subst-δ , sub m lt ⟩ ⟩
 ```
 
-* Case `var`: We have subst `σ M ≡ y`, so `M` must also be a variable, say `x`.
+* Case `var`: We have `subst σ M ≡ y`, so `M` must also be a variable, say `x`.
   We apply the lemma `subst-reflect-var` to conclude.
 
 * Case `↦-elim`: We have `subst σ M ≡ L₁ · L₂`. We proceed by cases on `M`.