diff options
| -rw-r--r-- | BFF.agda | 4 | ||||
| -rw-r--r-- | Bidir.agda | 3 | ||||
| -rw-r--r-- | FreeTheorems.agda | 2 | ||||
| -rw-r--r-- | Precond.agda | 5 |
4 files changed, 1 insertions, 13 deletions
@@ -11,11 +11,7 @@ open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open import Data.List using (List ; [] ; _∷_ ; map ; length) open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_) open import Function using (id ; _∘_ ; flip) -open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪) open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid) -open import Relation.Binary.PropositionalEquality using (cong) renaming (setoid to EqSetoid) -open Injection using (to) open import FinMap open import Generic using (mapMV ; ≡-to-Π) @@ -18,9 +18,6 @@ open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate ; map-cong ; map-∘) open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) open import Function using (id ; _∘_ ; flip) -open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Function.Injection using (module Injection) renaming (Injection to _↪_) -open Injection using (to) open import Relation.Binary.Core using (refl ; _≡_) open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid ; module ≡-Reasoning) renaming (setoid to EqSetoid) diff --git a/FreeTheorems.agda b/FreeTheorems.agda index 2181163..d4eb174 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -11,8 +11,6 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming open import Relation.Binary using (Setoid) open Injection using (to) -open import Generic using (≡-to-Π) - import GetTypes module ListList where diff --git a/Precond.agda b/Precond.agda index 81c204b..ebb5412 100644 --- a/Precond.agda +++ b/Precond.agda @@ -20,11 +20,8 @@ open Data.List.Any.Membership-≡ using (_∉_) open import Data.Maybe using (just) open import Data.Product using (∃ ; _,_ ; proj₂) open import Function using (flip ; _∘_ ; id) -open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Function.Injection using (module Injection) renaming (Injection to _↪_) -open Injection using (to) open import Relation.Binary using (Setoid) -open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) renaming (setoid to EqSetoid) +open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import Relation.Nullary using (yes ; no) |