From a8377f1d2e7749516c24712c0630baf4b4d40a88 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Thu, 25 Nov 2021 19:09:11 -0300 Subject: [PATCH] updated to new agda stdlib --- src/CLT.agda | 2 +- src/Lib.agda | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/CLT.agda b/src/CLT.agda index 16cf485..71a2755 100644 --- a/src/CLT.agda +++ b/src/CLT.agda @@ -207,6 +207,6 @@ module SetoidUtil where Tms a ._≈ₑ_ = _≈_ Tms a .isEquivalence = EqClosureIsEquivalence _⟶_ - open import Relation.Binary.SetoidReasoning public + open import Relation.Binary.Reasoning.MultiSetoid public open SetoidUtil public diff --git a/src/Lib.agda b/src/Lib.agda index f085050..accc197 100644 --- a/src/Lib.agda +++ b/src/Lib.agda @@ -20,6 +20,8 @@ open import Relation.Binary.Construct.Closure.ReflexiveTransitive open import Relation.Binary.Construct.Closure.Equivalence using (EqClosure ; symmetric) renaming (isEquivalence to EqClosureIsEquivalence) public +open import Relation.Binary.Construct.Closure.Symmetric + using (fwd; bwd) public open import Data.Sum using (_⊎_ ; inj₁ ; inj₂) public open import Data.Sum