------------------------------------------------------------------------
-- The Agda standard library
--
-- Type constructors giving rise to a semigroup at every type
-- e.g. (List, _++_)
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Effect.Choice where

open import Level

private
  variable
    ℓ ℓ′ : Level
    A  : Set ℓ

record RawChoice (F : Set ℓ → Set ℓ′) : Set (suc ℓ ⊔ ℓ′) where
  infixr  _<|>_ _∣_
  field
    _<|>_ : F A → F A → F A

  -- backwards compatibility: unicode variants
  _∣_ : F A → F A → F A
  _∣_ = _<|>_