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

Changed imports for Agda 2.6.0; moved Acknowledgements to top-level folder

Browse source
This commit is contained in:
Wen Kokke 2019-06-04 22:38:02 +01:00
parent f283c1fcbd
commit 3da844c239
8 changed files with 8 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

0
src/plfa/Acknowledgements.lagda → acknowledgements.md
View file

5
src/plfa/Inference.lagda
View file

@ -250,9 +250,8 @@ We are now ready to begin the formal development.
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.String using (String)
open import Data.String.Unsafe using (_≟_)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.String using (String; _≟_)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary using (¬_; Dec; yes; no)
\end{code}

3
src/plfa/Lambda.lagda
View file

@ -53,8 +53,7 @@ four.
\begin{code}
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Data.String using (String)
open import Data.String.Unsafe using (_≟_)
open import Data.String using (String; _≟_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Nullary using (Dec; yes; no; ¬_)

3
src/plfa/Properties.lagda
View file

@ -22,8 +22,7 @@ sequences for us.
\begin{code}
open import Relation.Binary.PropositionalEquality
using (_≡_; _≢_; refl; sym; cong; cong₂)
open import Data.String using (String)
open import Data.String.Unsafe using (_≟_)
open import Data.String using (String; _≟_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product

3
tspl/Assignment4.lagda
View file

@ -42,8 +42,7 @@ open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.String using (String)
open import Data.String.Unsafe using (_≟_)
open import Data.String using (String; _≟_)
open import Relation.Nullary using (¬_; Dec; yes; no)
\end{code}

3
tspl/Exam.lagda
View file

@ -25,8 +25,7 @@ open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc)
open import Data.List using (List; []; _∷_; _++_)
open import Data.Product using (∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.String using (String)
open import Data.String.Unsafe using (_≟_)
open import Data.String using (String; _≟_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary using (Decidable)
\end{code}

3
tspl/PUC-Assignment4.lagda
View file

@ -39,8 +39,7 @@ open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.String using (String)
open import Data.String.Unsafe using (_≟_)
open import Data.String using (String; _≟_)
open import Relation.Nullary using (¬_; Dec; yes; no)
\end{code}

3
tspl/PUC-Assignment5.lagda
View file

@ -39,8 +39,7 @@ open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.String using (String)
open import Data.String.Unsafe using (_≟_)
open import Data.String using (String; _≟_)
open import Relation.Nullary using (¬_; Dec; yes; no)
\end{code}