diff --git a/courses/tspl/2019/Assignment4.lagda.md b/courses/tspl/2019/Assignment4.lagda.md index 89c3dd10..dd4179df 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 ] Γ , y ⦂ B ∋ x ⦂ A ) + → ¬ (∃[ A ]( Γ ∋ 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} @@ -1022,12 +1022,12 @@ Remember to indent all code by two spaces. ``` synthesize : ∀ (Γ : Context) (M : Term⁺) - ----------------------- - → Dec (∃[ A ](Γ ⊢ M ↑ A)) + ----------------------- + → Dec (∃[ A ]( Γ ⊢ M ↑ A )) inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type) - --------------- - → Dec (Γ ⊢ M ↓ A) + --------------- + → Dec (Γ ⊢ M ↓ A) synthesize Γ (` x) with lookup Γ x ... | no ¬∃ = no (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ }) diff --git a/stack.yaml b/stack.yaml index 0a7399d6..45c8f85a 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,7 +1,7 @@ resolver: lts-17.2 -# Use GHC 8.10.3 -compiler: ghc-8.10.3 +# Use GHC 8.10.5 +compiler: ghc-8.10.5 compiler-check: match-exact # Allow never versions of packages