Tspl 2024 10 11

courses/TSPL/2024/Assignment1.lagda.md

@@ -45,7 +45,7 @@ module Naturals where
   import Relation.Binary.PropositionalEquality as Eq
   open Eq using (_≡_; refl)
   open Eq.≡-Reasoning using (begin_; step-≡-∣; _∎)
-  open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)
+  open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
 ```
 
 #### Exercise `seven` (practice) {#seven}
@@ -169,7 +169,7 @@ and some operations upon them.  We also require a couple of new operations,
   import Relation.Binary.PropositionalEquality as Eq
   open Eq using (_≡_; refl; cong; sym)
   open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎)
-  open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
+  open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)
   open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)
 ```
 (Importing `step-≡` defines `_≡⟨_⟩_`.)

courses/TSPL/2024/tspl.md

@@ -122,7 +122,7 @@ Not all students are expected to attempt the project.
 For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).
 
 * [Assignment 1](/TSPL/2024/Assignment1/) cw1 due 12 noon Friday 18 October (Week 5)
-* Assignment 2 cw2 due 12 noon Friday 1 November (Week 7)
+* [Assignment 2](/TSPL/2024/Assignment2/) cw2 due 12 noon Friday 1 November (Week 7)
 * Assignment 3 cw3 due 12 noon Friday 15 November (Week 9)
 * Assignment 4 cw4 due 12 noon Friday 29 November (Week 11)
 * Essay cw5 due 12 noon Thursday 23 January 2025 (Week 2, Semester 2)
@@ -155,6 +155,20 @@ submit tspl cwN AssignmentN.lagda.md
 where N is the number of the assignment. -->
 
 
+## Good Scholarly Practice.
+
+Please remember the University requirement as
+regards all assessed work. Details about this can be found at:
+
+> [https://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct](https://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct)
+
+You are required to take reasonable measures to protect
+your assessed work from unauthorised access. For example, if you put
+any such work on a public repository then you must set access
+permissions appropriately (generally permitting access only to
+yourself). Do not publish solutions to the coursework.
+
+
 ## Project
 
 The optional project is to take a research paper and formalise all or

src/plfa/part1/Connectives.lagda.md

@@ -30,8 +30,8 @@ principle known as _Propositions as Types_:
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
 open Eq.≡-Reasoning
-open import Data.Nat.Base using (ℕ)
-open import Function.Base using (_∘_)
+open import Data.Nat using (ℕ)
+open import Function using (_∘_)
 open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality; _⇔_)
 open plfa.part1.Isomorphism.≃-Reasoning
 ```

src/plfa/part1/Decidable.lagda.md

@@ -22,13 +22,13 @@ of a new notion of _decidable_.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
 open Eq.≡-Reasoning
-open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Product.Base using (_×_) renaming (_,_ to ⟨_,_⟩)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Relation.Nullary.Negation as Neg using (¬_)
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Relation.Nullary.Negation using (¬_)
   renaming (contradiction to ¬¬-intro)
 open import Data.Unit using (⊤; tt)
-open import Data.Empty using (⊥)
+open import Data.Empty using (⊥; ⊥-elim)
 open import plfa.part1.Relations using (_<_; z<s; s<s)
 open import plfa.part1.Isomorphism using (_⇔_)
 ```
@@ -509,7 +509,7 @@ we can decide if the first implies the second:
 ```agda
 _→-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A → B)
 _     →-dec yes y  =  yes (λ _ → y)
-no ¬x →-dec _      =  yes (λ x → Neg.contradiction x ¬x)
+no ¬x →-dec _      =  yes (λ x → ⊥-elim (¬x x))
 yes x →-dec no ¬y  =  no (λ f → ¬y (f x))
 ```
 The implication holds if either the second holds or

src/plfa/part1/Induction.lagda.md

@@ -26,7 +26,7 @@ and some operations upon them.  We also require a couple of new operations,
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; cong; sym)
 open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎)
-open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_;_^_)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)
 ```
 (Importing `step-≡-∣` defines `_≡⟨⟩_` and importing `step-≡-⟩` defines `_≡⟨_⟩_`.)
 

src/plfa/part1/Lists.lagda.md

@@ -17,13 +17,13 @@ examples of polymorphic types and higher-order functions.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
 open Eq.≡-Reasoning
-open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
-open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
+open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
 open import Data.Nat.Properties using
   (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ; *-distribʳ-+)
 open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Data.Product.Base using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
-open import Function.Base using (_∘_)
+open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
+open import Function using (_∘_)
 open import Level using (Level)
 open import plfa.part1.Isomorphism using (_≃_; _⇔_)
 ```

src/plfa/part1/Negation.lagda.md

@@ -14,10 +14,10 @@ and classical logic.
 
 ```agda
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Nat using (ℕ; zero; suc)
 open import Data.Empty using (⊥)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Data.Product.Base using (_×_)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Product using (_×_)
 open import Relation.Nullary.Negation using (contradiction)
 open import plfa.part1.Isomorphism using (_≃_; extensionality)
 ```
@@ -404,6 +404,8 @@ Definitions similar to those in this chapter can be found in the standard librar
 import Relation.Nullary using (¬_)
 import Relation.Nullary.Negation using (contradiction; contraposition)
 ```
+The standard library uses `contradiction`, which combines our
+`¬-elim` and `⊥-elim`.
 
 ## Unicode
 

src/plfa/part1/Quantifiers.lagda.md

@@ -14,12 +14,12 @@ This chapter introduces universal and existential quantification.
 ```agda
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
-open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_)
-open import Relation.Nullary.Negation using (¬_)
-open import Data.Product.Base using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Relation.Nullary using (¬_)
+open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import plfa.part1.Isomorphism using (_≃_; extensionality; ∀-extensionality)
-open import Function.Base using (_∘_)
+open import Function using (_∘_)
 ```
 
 

src/plfa/part1/Relations.lagda.md

@@ -819,7 +819,7 @@ properties of `One`. It may also help to prove the following:
 
 Definitions similar to those in this chapter can be found in the standard library:
 ```agda
-import Data.Nat using (_≤_; z≤n; s≤s)
+import Data.Nat using (_≤_; z≤n; s≤s; _<_)
 import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
                                   +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
 ```