Fixed binding issues with existential syntax.

This commit is contained in:
Wen Kokke 2021-08-23 11:57:30 +01:00
parent a92e1a08c4
commit 7345c36d80
No known key found for this signature in database
GPG key ID: 7EB7DBBCEB539DB8
5 changed files with 21 additions and 21 deletions

View file

@ -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}

View file

@ -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)
---------------

View file

@ -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

View file

@ -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/
```
```

View file

@ -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)
---------------