From 7345c36d80367e1922a7993f3b354c4bbc1b9ca3 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Mon, 23 Aug 2021 11:57:30 +0100 Subject: [PATCH] Fixed binding issues with existential syntax. --- courses/tspl/2019/Assignment4.lagda.md | 8 ++++---- courses/tspl/2019/Exam.lagda.md | 8 ++++---- hs/Main.hs | 2 +- pdf/README.md | 4 ++-- src/plfa/part2/Inference.lagda.md | 20 ++++++++++---------- 5 files changed, 21 insertions(+), 21 deletions(-) diff --git a/courses/tspl/2019/Assignment4.lagda.md b/courses/tspl/2019/Assignment4.lagda.md index dd4179df..1e02b6f1 100644 --- a/courses/tspl/2019/Assignment4.lagda.md +++ b/courses/tspl/2019/Assignment4.lagda.md @@ -982,15 +982,15 @@ 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 ⟩ lookup : ∀ (Γ : Context) (x : Id) ------------------------ - → Dec (∃[ A ](Γ ∋ x ⦂ A)) + → Dec (∃[ A ]( Γ ∋ x ⦂ A )) lookup ∅ x = no (λ ()) lookup (Γ , y ⦂ B) x with x ≟ y ... | yes refl = yes ⟨ B , Z ⟩ @@ -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} diff --git a/courses/tspl/2019/Exam.lagda.md b/courses/tspl/2019/Exam.lagda.md index 9d230954..d6abcef6 100644 --- a/courses/tspl/2019/Exam.lagda.md +++ 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} @@ -631,7 +631,7 @@ module Problem3 where ``` synthesize : ∀ (Γ : Context) (M : Term⁺) ----------------------- - → Dec (∃[ A ](Γ ⊢ M ↑ A)) + → Dec (∃[ A ]( Γ ⊢ M ↑ A )) inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type) --------------- diff --git a/hs/Main.hs b/hs/Main.hs index c99890dd..3274df47 100644 --- a/hs/Main.hs +++ b/hs/Main.hs @@ -257,7 +257,7 @@ main = do >>= loadAndApplyTemplate "templates/page.html" siteContext >>= loadAndApplyTemplate "templates/default.html" siteContext >>= prettifyUrls - + match "src/plfa/backmatter/acknowledgements.md" $ version "raw" $ do route $ constRoute "acknowledgements.md" compile $ getResourceBody diff --git a/pdf/README.md b/pdf/README.md index 515dc925..ce9d3dcb 100644 --- a/pdf/README.md +++ b/pdf/README.md @@ -7,7 +7,7 @@ Dependencies (relative to the root): - `README.md` - the font `DejaVu mononoki Symbola Droid` installed globally. (Could change to local?) -First, run `stack build && stack exec site rebuild` from the parent directory to generate acknowledgements.md under `_site`, which is needed by the pdf (Only need to do this once). +First, run `stack build && stack exec site rebuild` from the parent directory to generate acknowledgements.md under `_site`, which is needed by the pdf (Only need to do this once). Then, running `make pdf` from the parent directory should be sufficient to compile the book. The book will be generated in this folder as `plfa.pdf`. @@ -17,4 +17,4 @@ Alternatively, makefile in this directory provide these options: all # Build plfa.pdf (can also run from the parent as "make pdf") plfa-sample.pdf # Build a shrinked version of the book for testing all_tex # generate all tex version of lagda files under tex/ -``` \ No newline at end of file +``` diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md index aa30552b..75cd6099 100644 --- a/src/plfa/part2/Inference.lagda.md +++ b/src/plfa/part2/Inference.lagda.md @@ -208,11 +208,11 @@ _decidable_: synthesize : ∀ (Γ : Context) (M : Term⁺) ----------------------- - → Dec (∃[ A ](Γ ⊢ M ↑ A)) + → Dec (∃[ A ]( Γ ⊢ M ↑ A )) inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type) - --------------- - → Dec (Γ ⊢ M ↓ A) + --------------- + → Dec (Γ ⊢ M ↓ A) Given context `Γ` and synthesised term `M`, we must decide whether there exists a type `A` such that `Γ ⊢ M ↑ A` holds, or its negation. @@ -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 ⟩ ``` @@ -597,8 +597,8 @@ there exists a type `A` such that `Γ ∋ x ⦂ A` holds, or its negation: ``` lookup : ∀ (Γ : Context) (x : Id) - ----------------------- - → Dec (∃[ A ](Γ ∋ x ⦂ A)) + ------------------------- + → Dec (∃[ A ]( Γ ∋ x ⦂ A )) lookup ∅ x = no (λ ()) lookup (Γ , y ⦂ B) x with x ≟ y ... | yes refl = yes ⟨ B , Z ⟩ @@ -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 @@ -686,8 +686,8 @@ and a type `A` and either returns evidence that `Γ ⊢ M ↓ A`, or its negation: ``` synthesize : ∀ (Γ : Context) (M : Term⁺) - ----------------------- - → Dec (∃[ A ](Γ ⊢ M ↑ A)) + --------------------------- + → Dec (∃[ A ]( Γ ⊢ M ↑ A )) inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type) ---------------