{-# OPTIONS --cubical-compatible #-}
module Foreign.Haskell.Maybe where
open import Level
open import Data.Maybe.Base as Data using (just; nothing)
private
variable
a : Level
A : Set a
data Maybe (A : Set a) : Set a where
just : A → Maybe A
nothing : Maybe A
{-# FOREIGN GHC type AgdaMaybe l a = Maybe a #-}
{-# COMPILE GHC Maybe = data AgdaMaybe (Just | Nothing) #-}
toForeign : Data.Maybe A → Maybe A
toForeign (just x) = just x
toForeign nothing = nothing
fromForeign : Maybe A → Data.Maybe A
fromForeign (just x) = just x
fromForeign nothing = nothing
{-# WARNING_ON_IMPORT
"Warning: Foreign.Haskell.Maybe was deprecated in v1.4.
Maybe is now an Agda builtin and does not need library support."
#-}
{-# WARNING_ON_USAGE Maybe
"Warning: Foreign.Haskell.Maybe's Maybe was deprecated in v1.4.
Maybe is now an Agda builtin and does not need library support."
#-}
{-# WARNING_ON_USAGE toForeign
"Warning: toForeign was deprecated in v1.4.
Maybe is now an Agda builtin and does not need library support."
#-}
{-# WARNING_ON_USAGE fromForeign
"Warning: fromForeign was deprecated in v1.4.
Maybe is now an Agda builtin and does not need library support."
#-}