From 5a2c34f2b9461ab49e6ba2802a007da39beec521 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Fri, 11 Oct 2024 13:02:27 +0100 Subject: [PATCH 1/2] update Assignment2, remove Base --- courses/TSPL/2024/Assignment1.lagda.md | 4 ++-- src/plfa/part1/Connectives.lagda.md | 4 ++-- src/plfa/part1/Decidable.lagda.md | 12 ++++++------ src/plfa/part1/Induction.lagda.md | 2 +- src/plfa/part1/Lists.lagda.md | 8 ++++---- src/plfa/part1/Negation.lagda.md | 8 +++++--- src/plfa/part1/Quantifiers.lagda.md | 10 +++++----- src/plfa/part1/Relations.lagda.md | 2 +- 8 files changed, 26 insertions(+), 24 deletions(-) diff --git a/courses/TSPL/2024/Assignment1.lagda.md b/courses/TSPL/2024/Assignment1.lagda.md index 8651b4d15..5c2c75827 100644 --- a/courses/TSPL/2024/Assignment1.lagda.md +++ b/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 `_≡⟨_⟩_`.) diff --git a/src/plfa/part1/Connectives.lagda.md b/src/plfa/part1/Connectives.lagda.md index a36c6d2b0..922d0833a 100644 --- a/src/plfa/part1/Connectives.lagda.md +++ b/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 ``` diff --git a/src/plfa/part1/Decidable.lagda.md b/src/plfa/part1/Decidable.lagda.md index 601d0f456..7a1dfd84e 100644 --- a/src/plfa/part1/Decidable.lagda.md +++ b/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 Date: Fri, 11 Oct 2024 14:28:28 +0100 Subject: [PATCH 2/2] this time saving tspl.md --- courses/TSPL/2024/tspl.md | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/courses/TSPL/2024/tspl.md b/courses/TSPL/2024/tspl.md index 55d2a99c0..83ddfba77 100644 --- a/courses/TSPL/2024/tspl.md +++ b/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