module Haskell.Prim.Maybe where

--------------------------------------------------
-- Maybe

data Maybe {@0 } (a : Set ) : Set  where
  Nothing : Maybe a
  Just    : a -> Maybe a

maybe :  {@0 ℓ₁ ℓ₂} {@0 a : Set ℓ₁} {@0 b : Set ℓ₂}  b  (a  b)  Maybe a  b
maybe n j Nothing  = n
maybe n j (Just x) = j x

fromMaybe : {a : Set}  a  Maybe a  a
fromMaybe d Nothing = d
fromMaybe _ (Just x) = x