    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The Maybe type and some operations
    ------------------------------------------------------------------------

    -- The definitions in this file are reexported by Data.Maybe.

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Maybe.Base where

    open import Level using (Level; Lift)
    open import Data.Bool.Base using (Bool; true; false; not)
    open import Data.Unit.Base using (⊤)
    open import Data.These.Base using (These; this; that; these)
    open import Data.Product.Base as Prod using (_×_; _,_)
    open import Function.Base using (_∘_; id; const)
    import Relation.Nullary.Decidable.Core as Dec

    private
      variable
        a b c : Level
        A : Set a
        B : Set b
        C : Set c

    ------------------------------------------------------------------------
    -- Definition

    open import Agda.Builtin.Maybe public
      using (Maybe; just; nothing)

    ------------------------------------------------------------------------
    -- Some operations

    boolToMaybe : Bool → Maybe ⊤
    boolToMaybe true  = just _
    boolToMaybe false = nothing

    is-just : Maybe A → Bool
    is-just (just _) = true
    is-just nothing  = false

    is-nothing : Maybe A → Bool
    is-nothing = not ∘ is-just

    -- A dependent eliminator.

    maybe : ∀ {A : Set a} {B : Maybe A → Set b} →
            ((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x
    maybe j n (just x) = j x
    maybe j n nothing  = n

    -- A non-dependent eliminator.

    maybe′ : (A → B) → B → Maybe A → B
    maybe′ = maybe

    -- A defaulting mechanism

    fromMaybe : A → Maybe A → A
    fromMaybe = maybe′ id

    -- A safe variant of "fromJust". If the value is nothing, then the
    -- return type is the unit type.

    module _ {a} {A : Set a} where

      From-just : Maybe A → Set a
      From-just (just _) = A
      From-just nothing  = Lift a ⊤

      from-just : (x : Maybe A) → From-just x
      from-just (just x) = x
      from-just nothing  = _

    -- Functoriality: map

    map : (A → B) → Maybe A → Maybe B
    map f = maybe (just ∘ f) nothing

    -- Applicative: ap

    ap : Maybe (A → B) → Maybe A → Maybe B
    ap nothing  = const nothing
    ap (just f) = map f

    -- Monad: bind

    infixl 1 _>>=_
    _>>=_ : Maybe A → (A → Maybe B) → Maybe B
    nothing >>= f = nothing
    just a  >>= f = f a

    -- Alternative: <∣>

    infixr 6 _<∣>_
    _<∣>_ : Maybe A → Maybe A → Maybe A
    just x  <∣> my = just x
    nothing <∣> my = my

    -- Just when the boolean is true

    when : Bool → A → Maybe A
    when b c = map (const c) (boolToMaybe b)

    ------------------------------------------------------------------------
    -- Aligning and zipping

    alignWith : (These A B → C) → Maybe A → Maybe B → Maybe C
    alignWith f (just a) (just b) = just (f (these a b))
    alignWith f (just a) nothing  = just (f (this a))
    alignWith f nothing  (just b) = just (f (that b))
    alignWith f nothing  nothing  = nothing

    zipWith : (A → B → C) → Maybe A → Maybe B → Maybe C
    zipWith f (just a) (just b) = just (f a b)
    zipWith _ _        _        = nothing

    align : Maybe A → Maybe B → Maybe (These A B)
    align = alignWith id

    zip : Maybe A → Maybe B → Maybe (A × B)
    zip = zipWith _,_

    ------------------------------------------------------------------------
    -- Injections.

    thisM : A → Maybe B → These A B
    thisM a = maybe′ (these a) (this a)

    thatM : Maybe A → B → These A B
    thatM = maybe′ these that

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.1
    -- decToMaybe

    open Dec using (decToMaybe) public