Updated courses after f20abd92eb

courses/puc/2019/Assignment1.lagda.md

@@ -31,7 +31,7 @@ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
   ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
-open import plfa.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
+open import plfa.part1.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
 ```
 
 ## Naturals

courses/puc/2019/Assignment2.lagda.md

@@ -31,7 +31,6 @@ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
   ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
-open import plfa.Relations using (_<_; z<s; s<s)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 open import Data.Product using (Σ; ∃; Σ-syntax; ∃-syntax)
 open import Data.Unit using (⊤; tt)
@@ -47,10 +46,10 @@ open import Relation.Nullary.Negation using (contraposition)
 open import Relation.Unary using (Decidable)
 open import Function using (_∘_)
 open import Level using (Level)
-open import plfa.Relations using (_<_; z<s; s<s)
-open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
-open plfa.Isomorphism.≃-Reasoning
-open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
+open import plfa.part1.Relations using (_<_; z<s; s<s)
+open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.part1.Isomorphism.≃-Reasoning
+open import plfa.part1.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
   _++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
 ```
 

courses/puc/2019/Assignment3.lagda.md

@@ -39,13 +39,13 @@ open import Function using (_∘_)
 open import Algebra.Structures using (IsMonoid)
 open import Level using (Level)
 open import Relation.Unary using (Decidable)
-open import plfa.Relations using (_<_; z<s; s<s)
-open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
-open plfa.Isomorphism.≃-Reasoning
-open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
+open import plfa.part1.Relations using (_<_; z<s; s<s)
+open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.part1.Isomorphism.≃-Reasoning
+open import plfa.part1.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
   _++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
-open import plfa.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
-open import plfa.Properties hiding (value?; unstuck; preserves; wttdgs)
+open import plfa.part2.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
+open import plfa.part2.Properties hiding (value?; unstuck; preserves; wttdgs)
 ```
 
 ## Lambda

courses/puc/2019/Assignment4.lagda.md

@@ -54,7 +54,7 @@ module DeBruijn where
 Remember to indent all code by two spaces.
 
 ```
-  open import plfa.DeBruijn
+  open import plfa.part2.DeBruijn
 ```
 
 

courses/puc/2019/Assignment5.lagda.md

@@ -55,7 +55,7 @@ Remember to indent all code by two spaces.
 ### Imports
 
 ```
-  import plfa.More as DB
+  import plfa.part2.More as DB
 ```
 
 ### Syntax

courses/tspl/2018/Assignment1.lagda.md

@@ -34,7 +34,7 @@ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
   ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
-open import plfa.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
+open import plfa.part1.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
 ```
 
 ## Naturals

courses/tspl/2018/Assignment2.lagda.md

@@ -34,7 +34,6 @@ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
   ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
-open import plfa.Relations using (_<_; z<s; s<s)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 open import Data.Unit using (⊤; tt)
 open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
@@ -47,9 +46,9 @@ open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Nullary.Sum using (_⊎-dec_)
 open import Relation.Nullary.Negation using (contraposition)
 open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
-open import plfa.Relations using (_<_; z<s; s<s)
-open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
-open plfa.Isomorphism.≃-Reasoning
+open import plfa.part1.Relations using (_<_; z<s; s<s)
+open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.part1.Isomorphism.≃-Reasoning
 ```
 
 ## Equality

courses/tspl/2018/Assignment3.lagda.md

@@ -42,13 +42,13 @@ open import Function using (_∘_)
 open import Algebra.Structures using (IsMonoid)
 open import Level using (Level)
 open import Relation.Unary using (Decidable)
-open import plfa.Relations using (_<_; z<s; s<s)
-open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
-open plfa.Isomorphism.≃-Reasoning
-open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
+open import plfa.part1.Relations using (_<_; z<s; s<s)
+open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.part1.Isomorphism.≃-Reasoning
+open import plfa.part1.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
   _++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
-open import plfa.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
-open import plfa.Properties hiding (value?; unstuck; preserves; wttdgs)
+open import plfa.part2.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
+open import plfa.part2.Properties hiding (value?; unstuck; preserves; wttdgs)
 ```
 
 #### Exercise `reverse-++-commute` (recommended)

courses/tspl/2018/Assignment4.lagda.md

@@ -57,7 +57,7 @@ module DeBruijn where
 Remember to indent all code by two spaces.
 
 ```
-  open import plfa.DeBruijn
+  open import plfa.part2.DeBruijn
 ```
 
 
@@ -770,7 +770,7 @@ Remember to indent all code by two spaces.
 ### Imports
 
 ```
-  import plfa.More as DB
+  import plfa.part2.More as DB
 ```
 
 ### Syntax

courses/tspl/2018/Exam.lagda.md

@@ -398,7 +398,7 @@ module Problem3 where
 ### Imports
 
 ```
-  import plfa.DeBruijn as DB
+  import plfa.part2.DeBruijn as DB
 ```
 
 ### Syntax