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

Decidable: removes unused and unrelated imports

Browse source
This commit is contained in:
Marko Dimjašević 2019-03-10 18:56:46 +01:00 committed by Wen Kokke
parent 211368cf29
commit 0d020a2a33
1 changed files with 2 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/plfa/Decidable.lagda
View file

@ -23,18 +23,16 @@ of a new notion of _decidable_.
\begin{code}
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
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 using (¬_)
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Nullary.Negation using ()
renaming (contradiction to ¬¬-intro)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List using (List; []; _∷_; foldr; map)
open import Function using (_∘_)
open import plfa.Relations using (_<_; z<s; s<s)
open import plfa.Isomorphism using (_⇔_)
\end{code}
@ -568,7 +566,6 @@ postulate
\begin{code}
import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
import Data.Nat using (_≤?_)
import Data.List.All using (All; []; _∷_) renaming (all to All?)
import Relation.Nullary using (Dec; yes; no)
import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness)
import Relation.Nullary.Negation using (¬?)