michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fixed assignment 4.

Browse source
This commit is contained in:
Wen Kokke 2021-08-23 00:48:01 +01:00
parent 73fdcf34bd
commit a92e1a08c4
No known key found for this signature in database
GPG key ID: 7EB7DBBCEB539DB8
2 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
courses/tspl/2019/Assignment4.lagda.md
View file

@ -982,15 +982,15 @@ Remember to indent all code by two spaces.
``` ```
ext∋ : ∀ {Γ B x y} ext∋ : ∀ {Γ B x y}
→ 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∋ x≢y _ ⟨ A , Z ⟩ = x≢y refl
ext∋ _ ¬∃ ⟨ A , S _ ⊢x ⟩ = ¬∃ ⟨ A , ⊢x ⟩ ext∋ _ ¬∃ ⟨ A , S _ ⊢x ⟩ = ¬∃ ⟨ A , ⊢x ⟩
lookup : ∀ (Γ : Context) (x : Id) lookup : ∀ (Γ : Context) (x : Id)
----------------------- ------------------------
→ Dec (∃[ A ](Γ ∋ x ⦂ A)) → Dec (∃[ A ](Γ ∋ x ⦂ A))
lookup ∅ x = no (λ ()) lookup ∅ x = no (λ ())
lookup (Γ , y ⦂ B) x with x ≟ y lookup (Γ , y ⦂ B) x with x ≟ y
... | yes refl = yes ⟨ B , Z ⟩ ... | yes refl = yes ⟨ B , Z ⟩
@ -1006,7 +1006,7 @@ Remember to indent all code by two spaces.
→ Γ ⊢ L ↑ A ⇒ B → Γ ⊢ L ↑ A ⇒ B
→ ¬ Γ ⊢ M ↓ A → ¬ Γ ⊢ M ↓ A
---------------------------- ----------------------------
→ ¬ ( ∃[ B′ ] Γ ⊢ L · M ↑ B′ ) → ¬ (∃[ B′ ]( Γ ⊢ L · M ↑ B′ ))
¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′ ¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
¬switch : ∀ {Γ M A B} ¬switch : ∀ {Γ M A B}
@ -1022,12 +1022,12 @@ Remember to indent all code by two spaces.
``` ```
synthesize : ∀ (Γ : Context) (M : Term⁺) synthesize : ∀ (Γ : Context) (M : Term⁺)
----------------------- -----------------------
→ Dec (∃[ A ](Γ ⊢ M ↑ A)) → Dec (∃[ A ]( Γ ⊢ M ↑ A ))
inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type) inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
--------------- ---------------
→ Dec (Γ ⊢ M ↓ A) → Dec (Γ ⊢ M ↓ A)
synthesize Γ (` x) with lookup Γ x synthesize Γ (` x) with lookup Γ x
... | no ¬∃ = no (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ }) ... | no ¬∃ = no (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })

4
stack.yaml
View file

@ -1,7 +1,7 @@
resolver: lts-17.2 resolver: lts-17.2
# Use GHC 8.10.3 # Use GHC 8.10.5
compiler: ghc-8.10.3 compiler: ghc-8.10.5
compiler-check: match-exact compiler-check: match-exact
# Allow never versions of packages # Allow never versions of packages