Merge branch 'dev' of github.com:plfa/plfa.github.io into dev

2021-08-10 17:51:19 +01:00 · 2021-08-10 17:51:19 +01:00 · a162bcee5e
commit a162bcee5e
parent effcfb1e3e f7bc29d6f0
10 changed files with 118 additions and 127 deletions
--- a/2
+++ b/2
@ -12,7 +12,7 @@ TMP_DIR := $(CACHE_DIR)/tmp
 #################################################################################

 .PHONY: init
-init: setup-check-fix-whitespace setup-check-htmlproofer
+init: setup-check-fix-whitespace setup-install-htmlproofer
 	git config core.hooksPath .githooks


--- a/courses/tspl/2019/Assignment4.lagda.md
+++ b/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 ⟩

@ -1005,8 +1005,8 @@ Remember to indent all code by two spaces.
  ¬arg : ∀ {Γ A B L M}
    → Γ ⊢ 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}
--- a/courses/tspl/2019/Exam.lagda.md
+++ b/courses/tspl/2019/Exam.lagda.md
@ -589,13 +589,14 @@ 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 ⟩

-  lookup : ∀ (Γ : Context) (x : Id)
+  lookup :
+      ∀ (Γ : Context) (x : Id)
      -----------------------
    → Dec (∃[ A ](Γ ∋ x ⦂ A))
  lookup ∅ x                        =  no  (λ ())
@ -612,8 +613,8 @@ module Problem3 where
  ¬arg : ∀ {Γ A B L M}
    → Γ ⊢ 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}
--- a/css/epub.css
+++ b/css/epub.css
@ -4,19 +4,19 @@
    font-family: 'mononoki';
    font-weight: normal;
    font-style: normal;
-    src: url('../fonts/mononoki.woff');
+    src: url('../webfonts/mononoki.woff');
 }
@font-face {
    font-family: 'FreeMono';
    font-weight: normal;
    font-style: normal;
-    src: url('../fonts/FreeMono.woff');
+    src: url('../webfonts/FreeMono.woff');
 }
@font-face {
    font-family: 'DejaVuSansMono';
    font-weight: normal;
    font-style: normal;
-    src: url('../fonts/DejaVuSansMono.woff');
+    src: url('../webfonts/DejaVuSansMono.woff');
 }
 body { margin: 5%; text-align: justify; font-size: medium; }
 code { font-family: 'mononoki', 'FreeMono', 'DejaVuSansMono', monospace; }
--- a/css/minima.scss
+++ b/css/minima.scss
@ -1,4 +1,5 @@
@import
    "minima/skins/classic",
-    "minima/initialize"
+    "minima/initialize",
+    "minima/agda"
 ;
--- a/css/minima/agda.scss
+++ b/css/minima/agda.scss
@ -1,19 +1,18 @@
@font-face {
    font-family: 'mononoki';
-    src: url('fonts/mononoki.woff2') format('woff2'),
-         url('fonts/mononoki.woff')  format('woff');
+    src: url('../webfonts/mononoki.woff2') format('woff2'),
+         url('../webfonts/mononoki.woff')  format('woff');
 }
@font-face {
    font-family: 'DejaVu Sans Mono';
-    src: url('fonts/DejaVuSansMono.woff2') format('woff2'),
-         url('fonts/DejaVuSansMono.woff') format('woff');
+    src: url('../webfonts/DejaVuSansMono.woff') format('woff');
    font-weight: normal;
    font-style: normal;

 }
@font-face {
    font-family: 'FreeMono';
-    src: url('fonts/FreeMono.woff') format('woff');
+    src: url('../webfonts/FreeMono.woff') format('woff');
    font-stretch: normal;
    font-style: normal;
    unicode-range: U+20-7E, U+A0-220, U+224-233, U+237, U+250-36F, U+374-375, U+37A, U+37E, U+384-38A, U+38C, U+38E-3A1, U+3A3-3CE, U+3D0-3D6, U+3DA-3DD, U+3F0-3F1, U+3F4-3F5, U+400-47F, U+483-487, U+48A-4FF, U+510-513, U+51A-51F, U+524-527, U+531-556, U+559-55F, U+561-587, U+589-58A, U+58F, U+5B0-5C7, U+5D0-5EA, U+5F0-5F4, U+606-60F, U+61B, U+61E-657, U+659-6D5, U+6EE-6FF, U+10D0-10F5, U+10F9, U+10FB-10FC, U+13A0-13F4, U+16A0-16F0, U+1E00-1E9B, U+1EA0-1EF9, U+1F00-1F15, U+1F18-1F1D, U+1F20-1F45, U+1F48-1F4D, U+1F50-1F57, U+1F59, U+1F5B, U+1F5D, U+1F5F-1F7D, U+1F80-1FB4, U+1FB6-1FC4, U+1FC6-1FD3, U+1FD6-1FDB, U+1FDD-1FEF, U+1FF2-1FF4, U+1FF6-1FFE, U+2000-2064, U+20A1-20B5, U+20B8-20B9, U+20D0-20D2, U+20D6-20D7, U+20DB-20E3, U+20E5-20E6, U+20E8, U+20EA-20EF, U+2100-2109, U+210D-211A, U+211C-211E, U+2120-2122, U+2124, U+2126-2127, U+2129-212B, U+212E, U+2132, U+2135-213B, U+2141-2144, U+214B, U+214D-214E, U+2153-217F, U+2190-21D5, U+21DC-21DD, U+21E6-21E9, U+21F3, U+2200-22F1, U+2300, U+2302-2306, U+2308-2310, U+2312, U+2314-2315, U+2318-2319, U+231C-2327, U+2329-232C, U+2336-237A, U+237C-23B7, U+23BA-23CF, U+23DA-23DB, U+23DE-23DF, U+23E2-23E6, U+2400-2426, U+2440-244A, U+2460-2469, U+2500-2609, U+2610-2614, U+261A-261F, U+2626-2629, U+262E-2653, U+2660-2667, U+2669-266F, U+2680-2685, U+27C0-27CA, U+27CC, U+27D0-27D7, U+27E4-27EB, U+27F2-27F3, U+27F5-27FC, U+2800-28FF, U+2A00-2A06, U+2A1D, U+2A3F, U+2B00-2B0D, U+2B12-2B19, U+2B1B-2B2B, U+2B53-2B54, U+2E16-2E18, U+2E1A-2E1B, U+2E1E-2E1F, U+2E28-2E2E, U+2E30, U+A788-A78C, U+A900-A92F, U+FB00-FB05, U+FB1D-FB36, U+FB38-FB3C, U+FB3E, U+FB40-FB41, U+FB43-FB44, U+FB46-FBBE, U+FBC0-FBC1, U+FBD3-FBE9, U+FBFC-FBFF, U+FE70-FE74, U+FE76-FEFC, U+FEFF, U+FFF9-FFFD;
--- a/src/plfa/backmatter/Fonts.lagda.md
+++ b/src/plfa/backmatter/Fonts.lagda.md
@ -11,113 +11,101 @@ module plfa.backmatter.Fonts where

 Preferably, all vertical bars should line up.

-```
-{-
--------------------------|
-abcdefghijklmnopqrstuvwxyz|
-ABCDEFGHIJKLMNOPQRSTUVWXYZ|
-ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ|
-ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ   |
-ₐ   ₑ  ₕᵢⱼₖₗₘₙₒₚ ᵣₛₜᵤ  ₓ  |
--------------------------|
----------|
-0123456789|
-⁰¹²³⁴⁵⁶⁷⁸⁹|
-₀₁₂₃₄₅₆₇₈₉|
----------|
------------------------|
-αβγδεζηθικλμνξοπρστυφχψω|
-ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ|
------------------------|
----|
-≠≠≠≠|
-ηημμ|
-ΓΓΔΔ|
-ΣΣΠΠ|
-λλλλ|
-ƛƛƛƛ|
-····|
-××××|
-ℓℓℓℓ|
-≡≡≡≡|
-¬¬¬¬|
-≤≤≥≥|
-∅∅∅∅|
-————|
-††‡‡|
-^^^^|
-''""|
-``~~|
-⊎⊎⊃⊃|
-∧∧∨∨|
-⊗⊗⊗⊗|
-⊔⊔⊔⊔|
-cᶜbᵇ|
-lˡrʳ|
-⁻⁻⁺⁺|
-ℕℕℕℕ|
-∀∀∃∃|
-′′″″|
-∘∘∘∘|
-‌≢≢≃≃|
-≲≲≳≳|
-≟≟≐≐|
-∸∸∸∸|
-⟨⟨⟩⟩|
-⌊⌊⌋⌋|
-⌈⌈⌉⌉|
-↑↑↓↓|
-⇔⇔↔↔|
-→→⇒⇒|
-←←⇐⇐|
-↞↞↠↠|
-∈∈∋∋|
-⊢⊢⊣⊣|
-⊥⊥⊤⊤|
-∷∷∷∷|
-∎∎∎∎|
-⦂⦂⦂⦂|
-∥∥∥∥|
-★★★★|
-∌∌∉∉|
-⨟⨟⨟⨟|
-⨆⨆⨆⨆|
-〔〔〕〕|
----|
-}
-```
+    --------------------------|
+    abcdefghijklmnopqrstuvwxyz|
+    ABCDEFGHIJKLMNOPQRSTUVWXYZ|
+    ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ|
+    ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ   |
+    ₐ   ₑ  ₕᵢⱼₖₗₘₙₒₚ ᵣₛₜᵤ  ₓ  |
+    --------------------------|
+    ----------|
+    0123456789|
+    ⁰¹²³⁴⁵⁶⁷⁸⁹|
+    ₀₁₂₃₄₅₆₇₈₉|
+    ----------|
+    ------------------------|
+    αβγδεζηθικλμνξοπρστυφχψω|
+    ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ|
+    ------------------------|
+    ----|
+    ≠≠≠≠|
+    ηημμ|
+    ΓΓΔΔ|
+    ΣΣΠΠ|
+    λλλλ|
+    ƛƛƛƛ|
+    ····|
+    ××××|
+    ℓℓℓℓ|
+    ≡≡≡≡|
+    ¬¬¬¬|
+    ≤≤≥≥|
+    ∅∅∅∅|
+    ————|
+    ††‡‡|
+    ^^^^|
+    ''""|
+    ``~~|
+    ⊎⊎⊃⊃|
+    ∧∧∨∨|
+    ⊗⊗⊗⊗|
+    ⊔⊔⊔⊔|
+    cᶜbᵇ|
+    lˡrʳ|
+    ⁻⁻⁺⁺|
+    ℕℕℕℕ|
+    ∀∀∃∃|
+    ′′″″|
+    ∘∘∘∘|
+    ‌≢≢≃≃|
+    ≲≲≳≳|
+    ≟≟≐≐|
+    ∸∸∸∸|
+    ⟨⟨⟩⟩|
+    ⌊⌊⌋⌋|
+    ⌈⌈⌉⌉|
+    ↑↑↓↓|
+    ⇔⇔↔↔|
+    →→⇒⇒|
+    ←←⇐⇐|
+    ↞↞↠↠|
+    ∈∈∋∋|
+    ⊢⊢⊣⊣|
+    ⊥⊥⊤⊤|
+    ∷∷∷∷|
+    ∎∎∎∎|
+    ⦂⦂⦂⦂|
+    ∥∥∥∥|
+    ★★★★|
+    ∌∌∉∉|
+    ⨟⨟⨟⨟|
+    ⨆⨆⨆⨆|
+    〔〔〕〕|
+    ----|

 In the book we use the em-dash to make big arrows.

-```
-{-
----|
-—→—→|
-←—←—|
-↞—↞—|
-—↠—↠|
----|
-}
-```
+    ----|
+    —→—→|
+    ←—←—|
+    ↞—↞—|
+    —↠—↠|
+    ----|

 Here are some characters that are often not monospaced.

-```
-{-
----|
-😇😇|
-😈😈|
-⁗⁗|
-‴‴|
----|
------------|
------------|
----------|
-𝔸𝔹𝔻𝔼𝔽𝔾𝕀𝕁𝕂𝕃𝕄ℕ𝕆𝕊|
-𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛|
-𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘|
-ℰℱ|
----------|
+    ----|
+    😇😇|
+    😈😈|
+    ⁗⁗|
+    ‴‴|
+    ----|
+    ------------|
+    ------------|
+    ----------|
+    𝔸𝔹𝔻𝔼𝔽𝔾𝕀𝕁𝕂𝕃𝕄ℕ𝕆𝕊|
+    𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛|
+    𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘|
+    ℰℱ|
+    ----------|

-}
-```
--- a/src/plfa/index.md
+++ b/src/plfa/index.md
@ -41,6 +41,7 @@ $endfor$
  * [William Cook, University of Texas][UT-2020]
  * [Jeremy Siek, Indiana University][IU-2020]
  * [John Maraist, University of Wisconsin-La Crosse][UWL-2020]
+  * [Ugo de'Liguoro, Università di Torino][Torino-2020]

 #### 2019
  * [Dan Ghica, University of Birmingham][BHAM-2019]
@ -71,3 +72,4 @@ Please tell us of others!
 [SCP]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#scf
 [NextJournal]: https://nextjournal.com/plfa/ToC
 [UWL-2020]: https://github.com/jphmrst/PLC/tree/fall2020
+[Torino-2020]: http://laurea.educ.di.unito.it/index.php/offerta-formativa/insegnamenti/elenco-completo/elenco-completo/scheda-insegnamento?cod=MFN0633&codA=&year=2020&orienta=NSE
--- a/src/plfa/part2/Inference.lagda.md
+++ b/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 ⟩
 ```
@ -638,8 +638,8 @@ there is no term `B′` such that `Γ ⊢ L · M ↑ B′` holds:
 ¬arg : ∀ {Γ A B L M}
  → Γ ⊢ 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
--- a/2
+++ b/2
@ -1 +1 @@
-Subproject commit 9f929b4fe28bb7ba74b6b95d01ed0958343f3451
+Subproject commit 2f0fb515271fa1a01a5c55b9cf5d401c5c65aa37