2022-02-08 19:26:58 -05:00
|
|
|
module FFI.Data.Maybe where
|
|
|
|
|
2022-03-02 17:02:51 -05:00
|
|
|
open import Agda.Builtin.Equality using (_≡_; refl)
|
|
|
|
|
2022-02-08 19:26:58 -05:00
|
|
|
{-# FOREIGN GHC import qualified Data.Maybe #-}
|
|
|
|
|
|
|
|
data Maybe (A : Set) : Set where
|
|
|
|
nothing : Maybe A
|
|
|
|
just : A → Maybe A
|
|
|
|
{-# COMPILE GHC Maybe = data Data.Maybe.Maybe (Data.Maybe.Nothing|Data.Maybe.Just) #-}
|
2022-03-02 17:02:51 -05:00
|
|
|
|
|
|
|
just-inv : ∀ {A} {x y : A} → (just x ≡ just y) → (x ≡ y)
|
|
|
|
just-inv refl = refl
|
|
|
|
|