From 9691c05909c07fc8195f92a06d0cd92a858df02f Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Wed, 14 Jul 2021 16:50:25 +0100 Subject: [PATCH] Fixed Agda errors; fixed css errors which resulted in the incorrect font being used. --- Makefile | 2 +- courses/tspl/2019/Assignment4.lagda.md | 8 ++++---- courses/tspl/2019/Exam.lagda.md | 11 ++++++----- css/minima.scss | 6 +++--- css/{theme => minima}/_base.scss | 0 css/{theme => minima}/_layout.scss | 0 css/{theme => minima}/agda.scss | 0 css/{theme => minima}/custom-styles.scss | 0 css/{theme => minima}/custom-variables.scss | 0 css/{theme => minima}/initialize.scss | 0 css/{theme => minima}/skins/classic.scss | 0 css/{theme => minima}/skins/dark.scss | 0 css/{theme => minima}/skins/solarized-dark.scss | 0 css/{theme => minima}/skins/solarized.scss | 0 hs/Main.hs | 2 +- src/plfa/part2/Inference.lagda.md | 8 ++++---- 16 files changed, 19 insertions(+), 18 deletions(-) rename css/{theme => minima}/_base.scss (100%) rename css/{theme => minima}/_layout.scss (100%) rename css/{theme => minima}/agda.scss (100%) rename css/{theme => minima}/custom-styles.scss (100%) rename css/{theme => minima}/custom-variables.scss (100%) rename css/{theme => minima}/initialize.scss (100%) rename css/{theme => minima}/skins/classic.scss (100%) rename css/{theme => minima}/skins/dark.scss (100%) rename css/{theme => minima}/skins/solarized-dark.scss (100%) rename css/{theme => minima}/skins/solarized.scss (100%) 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/minima.scss b/css/minima.scss index d26997a8..a42fe7c1 100644 --- a/css/minima.scss +++ b/css/minima.scss @@ -1,5 +1,5 @@ @import - "theme/skins/classic", - "theme/initialize", - "theme/agda" + "minima/skins/classic", + "minima/initialize", + "minima/agda" ; diff --git a/css/theme/_base.scss b/css/minima/_base.scss similarity index 100% rename from css/theme/_base.scss rename to css/minima/_base.scss diff --git a/css/theme/_layout.scss b/css/minima/_layout.scss similarity index 100% rename from css/theme/_layout.scss rename to css/minima/_layout.scss diff --git a/css/theme/agda.scss b/css/minima/agda.scss similarity index 100% rename from css/theme/agda.scss rename to css/minima/agda.scss diff --git a/css/theme/custom-styles.scss b/css/minima/custom-styles.scss similarity index 100% rename from css/theme/custom-styles.scss rename to css/minima/custom-styles.scss diff --git a/css/theme/custom-variables.scss b/css/minima/custom-variables.scss similarity index 100% rename from css/theme/custom-variables.scss rename to css/minima/custom-variables.scss diff --git a/css/theme/initialize.scss b/css/minima/initialize.scss similarity index 100% rename from css/theme/initialize.scss rename to css/minima/initialize.scss diff --git a/css/theme/skins/classic.scss b/css/minima/skins/classic.scss similarity index 100% rename from css/theme/skins/classic.scss rename to css/minima/skins/classic.scss diff --git a/css/theme/skins/dark.scss b/css/minima/skins/dark.scss similarity index 100% rename from css/theme/skins/dark.scss rename to css/minima/skins/dark.scss diff --git a/css/theme/skins/solarized-dark.scss b/css/minima/skins/solarized-dark.scss similarity index 100% rename from css/theme/skins/solarized-dark.scss rename to css/minima/skins/solarized-dark.scss diff --git a/css/theme/skins/solarized.scss b/css/minima/skins/solarized.scss similarity index 100% rename from css/theme/skins/solarized.scss rename to css/minima/skins/solarized.scss diff --git a/hs/Main.hs b/hs/Main.hs index 20b2345d..ed3ad905 100644 --- a/hs/Main.hs +++ b/hs/Main.hs @@ -336,7 +336,7 @@ main = do -- Compile CSS match "css/*.css" $ compile compressCssCompiler - scss <- makePatternDependency "css/theme/**.scss" + scss <- makePatternDependency "css/minima/**.scss" rulesExtraDependencies [scss] $ match "css/minima.scss" $ compile $ sassCompilerWith sassOptions 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