small changes: Subtyping, Inference, Assignment 4, Exam

courses/tspl/2019/Assignment4.lagda.md

@@ -982,9 +982,9 @@ Remember to indent all code by two spaces.
 ```
   ext∋ : ∀ {Γ B x y}
     → x ≢ y
-    → ¬ ( ∃[ A ] Γ ∋ x ⦂ A )
+    → ¬ ∃[ A ]( Γ ∋ x ⦂ A )
       -----------------------------
-    → ¬ ( ∃[ A ] Γ , y ⦂ B ∋ x ⦂ A )
+    → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
   ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
   ext∋ _   ¬∃ ⟨ A , S _ ⊢x ⟩  =  ¬∃ ⟨ A , ⊢x ⟩
 
@@ -1006,7 +1006,7 @@ Remember to indent all code by two spaces.
     → Γ ⊢ L ↑ A ⇒ B
     → ¬ Γ ⊢ M ↓ A
       ----------------------------
-    → ¬ ( ∃[ B′ ] Γ ⊢ L · M ↑ B′ )
+    → ¬ ∃[ B′ ]( Γ ⊢ L · M ↑ B′ )
   ¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
 
   ¬switch : ∀ {Γ M A B}

courses/tspl/2019/Exam.lagda.md

@@ -589,9 +589,9 @@ module Problem3 where
 ```
   ext∋ : ∀ {Γ B x y}
     → x ≢ y
-    → ¬ ( ∃[ A ] Γ ∋ x ⦂ A )
+    → ¬ ∃[ A ]( Γ ∋ x ⦂ A )
       -----------------------------
-    → ¬ ( ∃[ A ] Γ , y ⦂ B ∋ x ⦂ A )
+    → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
   ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
   ext∋ _   ¬∃ ⟨ A , S _ ⊢x ⟩  =  ¬∃ ⟨ A , ⊢x ⟩
 
@@ -614,7 +614,7 @@ module Problem3 where
     → Γ ⊢ L ↑ A ⇒ B
     → ¬ Γ ⊢ M ↓ A
       ----------------------------
-    → ¬ ( ∃[ B′ ] Γ ⊢ L · M ↑ B′ )
+    → ¬ ∃[ B′ ]( Γ ⊢ L · M ↑ B′ )
   ¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
 
   ¬switch : ∀ {Γ M A B}

src/plfa/part2/DeBruijn.lagda.md

@@ -1388,3 +1388,12 @@ This chapter uses the following unicode:
     ₆  U+2086  SUBSCRIPT SIX (\_6)
     ₇  U+2087  SUBSCRIPT SEVEN (\_7)
     ≠  U+2260  NOT EQUAL TO (\=n)
+
+```
+mul : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
+mul = μ ƛ ƛ (case (# 1) `zero (plus · # 1 · (# 3 · # 0 · # 1)))
+```
+
+_ : eval (gas 100) (mul · two · two) ≡ [code generated by ctrl+c ctrl+n]
+
+_ = refl

src/plfa/part2/Inference.lagda.md

@@ -580,9 +580,9 @@ such that `Γ ∋ x ⦂ A` holds, then there is also no type `A` such that
 ```
 ext∋ : ∀ {Γ B x y}
   → x ≢ y
-  → ¬ ( ∃[ A ] Γ ∋ x ⦂ A )
+  → ¬ ∃[ A ]( Γ ∋ x ⦂ A )
     -----------------------------
-  → ¬ ( ∃[ A ] Γ , y ⦂ B ∋ x ⦂ A )
+  → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
 ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
 ext∋ _   ¬∃ ⟨ A , S _ ∋x ⟩  =  ¬∃ ⟨ A , ∋x ⟩
 ```
@@ -639,7 +639,7 @@ there is no term `B′` such that `Γ ⊢ L · M ↑ B′` holds:
   → Γ ⊢ L ↑ A ⇒ B
   → ¬ Γ ⊢ M ↓ A
     ----------------------------
-  → ¬ ( ∃[ B′ ] Γ ⊢ L · M ↑ B′ )
+  → ¬ ∃[ B′ ]( Γ ⊢ L · M ↑ B′ )
 ¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
 ```
 Let `⊢L` be evidence that `Γ ⊢ L ↑ A ⇒ B` holds and `¬⊢M` be evidence

src/plfa/part2/Subtyping.lagda.md

@@ -195,7 +195,7 @@ distinct? (x ∷ xs)
 ... | no x∉xs
     with distinct? xs
 ... | yes dxs = yes ⟨ x∉xs , dxs ⟩
-... | no ¬dxs = no λ x₁ → ¬dxs (proj₂ x₁)
+... | no ¬dxs = no λ z → ¬dxs (proj₂ z)
 ```
 
 With this decision procedure in hand, we define the following