ConcurrentSlicingCommon.agda

module ConcurrentSlicingCommon where

   open import Algebra.FunctionProperties public
   open import Algebra.Structures public
   open import Data.Bool public hiding (_≟_; decSetoid)
   open import Data.Empty public
   open import Data.Product public renaming (proj₁ to π₁; proj₂ to π₂; swap to ×-swap)
   open import Data.String public hiding (_≟_; decSetoid; setoid; show)
   open import Data.Sum public hiding (map)
   open import Data.Unit public hiding (_≟_; decSetoid; preorder; setoid; _≤_; module _≤_)
   open import Ext public hiding (_-×-_)
   open import Ext.Data.Product hiding (_,_) public
   open import Ext.Relation.Binary.PropositionalEquality public
   open import Ext.Relation.Binary.HeterogeneousEquality public
   open import Ext.Relation.Binary.PropositionalEquality public
   open import Function public renaming (_∘_ to _∘ᶠ_; id to idᶠ)
   open import IO public
   open import Relation.Nullary public
   open import Relation.Binary public
   open import Relation.Binary.PropositionalEquality public
   open import Relation.Binary.PropositionalEquality.TrustMe public
   open import Relation.Binary.HeterogeneousEquality as ᴴ public
      using (module ≅-Reasoning; ≅-to-≡; ≡-to-≅; subst-removable; ≡-subst-removable)
      renaming (
         _≅_ to _≅_; refl to ≅-refl; sym to ≅-sym; trans to ≅-trans;
         cong to ≅-cong; cong₂ to ≅-cong₂; subst to ≅-subst; subst₂ to ≅-subst₂
      )
   open import Size public