------------------------------------------------------------------------
-- The Agda standard library
--
-- Type constructors giving rise to a semigroup at every type
-- e.g. (List, _++_)
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --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
  _∣_ = _<|>_