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

miminimised imports for More

Browse source
This commit is contained in:
wadler 2018-07-09 21:36:16 -03:00
parent 554e0ed28e
commit a5fe099e9e
2 changed files with 4 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
extra/answers/MoreAns.lagda
View file

@ -24,14 +24,10 @@ and leave formalisation of the remaining constructs as an exercise.
\begin{code} \begin{code}
import Relation.Binary.PropositionalEquality as Eq import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong) open Eq using (_≡_; refl)
open import Data.Empty using (⊥; ⊥-elim) open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _*_) open import Data.Nat using (ℕ; zero; suc; _*_)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩) open import Relation.Nullary using (¬_)
open import Data.Unit using (⊤; tt)
open import Function using (_∘_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Nullary using (¬_; Dec; yes; no)
\end{code} \end{code}

8
src/plfa/More.lagda
View file

@ -559,14 +559,10 @@ and leave formalisation of the remaining constructs as an exercise.
\begin{code} \begin{code}
import Relation.Binary.PropositionalEquality as Eq import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong) open Eq using (_≡_; refl)
open import Data.Empty using (⊥; ⊥-elim) open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _*_) open import Data.Nat using (ℕ; zero; suc; _*_)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩) open import Relation.Nullary using (¬_)
open import Data.Unit using (⊤; tt)
open import Function using (_∘_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Nullary using (¬_; Dec; yes; no)
\end{code} \end{code}