------------------------------------------------------------------------
-- 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)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4