------------------------------------------------------------------------
-- The Agda standard library
--
-- An either-or-both data type
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.These where
 
open import Level
open import Data.Maybe.Base using (Maybe; just; nothing; maybe′)
open import Data.Sum.Base using (_⊎_; [_,_]′)
open import Function.Base using (const; _∘′_; id; constᵣ)
 
 
------------------------------------------------------------------------
-- Re-exporting the datatype and its operations
 
open import Data.These.Base public
 
private
  variable
    a b : Level
    A : Set a
    B : Set b
 
------------------------------------------------------------------------
-- Additional operations
 
-- projections
 
fromThis : These A B → Maybe A
fromThis = fold just (const nothing) (const ∘′ just)
 
fromThat : These A B → Maybe B
fromThat = fold (const nothing) just (const just)
 
leftMost : These A A → A
leftMost = fold id id const
 
rightMost : These A A → A
rightMost = fold id id constᵣ
 
mergeThese : (A → A → A) → These A A → A
mergeThese = fold id id
 
-- deletions
 
deleteThis : These A B → Maybe (These A B)
deleteThis = fold (const nothing) (just ∘′ that) (const (just ∘′ that))
 
deleteThat : These A B → Maybe (These A B)
deleteThat = fold (just ∘′ this) (const nothing) (const ∘′ just ∘′ this)