diff --git a/Makefile b/Makefile index f022d075..6f082466 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/courses/tspl/2019/Assignment4.lagda.md b/courses/tspl/2019/Assignment4.lagda.md index b2777e22..89c3dd10 100644 --- 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} diff --git a/courses/tspl/2019/Exam.lagda.md b/courses/tspl/2019/Exam.lagda.md index 0624dee2..9d230954 100644 --- 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} diff --git a/css/epub.css b/css/epub.css index d82bc875..1a8c1d0e 100644 --- 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; } diff --git a/css/minima.scss b/css/minima.scss index b5b5b84c..a42fe7c1 100644 --- a/css/minima.scss +++ b/css/minima.scss @@ -1,4 +1,5 @@ @import "minima/skins/classic", - "minima/initialize" + "minima/initialize", + "minima/agda" ; diff --git a/css/agda.css b/css/minima/agda.scss similarity index 93% rename from css/agda.css rename to css/minima/agda.scss index 2d7eb61f..d52f28a0 100644 --- a/css/agda.css +++ 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; diff --git a/src/plfa/backmatter/Fonts.lagda.md b/src/plfa/backmatter/Fonts.lagda.md index 8e98a68d..ae6e86ba 100644 --- 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. -``` -{- -----| -😇😇| -😈😈| -⁗⁗| -‴‴| -----| -------------| -------------| -----------| -𝔸𝔹𝔻𝔼𝔽𝔾𝕀𝕁𝕂𝕃𝕄ℕ𝕆𝕊| -𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛| -𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘| -ℰℱ| -----------| + ----| + 😇😇| + 😈😈| + ⁗⁗| + ‴‴| + ----| + ------------| + ------------| + ----------| + 𝔸𝔹𝔻𝔼𝔽𝔾𝕀𝕁𝕂𝕃𝕄ℕ𝕆𝕊| + 𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛| + 𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘| + ℰℱ| + ----------| --} -``` diff --git a/src/plfa/index.md b/src/plfa/index.md index 0b74c630..6f2dfbe9 100644 --- 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 diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md index 5be2978f..aa30552b 100644 --- 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 diff --git a/standard-library b/standard-library index 9f929b4f..2f0fb515 160000 --- a/standard-library +++ b/standard-library @@ -1 +1 @@ -Subproject commit 9f929b4fe28bb7ba74b6b95d01ed0958343f3451 +Subproject commit 2f0fb515271fa1a01a5c55b9cf5d401c5c65aa37