luau/prototyping/FFI/Data/Maybe.agda

module FFI.Data.Maybe where

open import Agda.Builtin.Equality using (_≡_; refl)

{-# 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) #-}

just-inv : ∀ {A} {x y : A} → (just x ≡ just y) → (x ≡ y)
just-inv refl = refl
Prototyping a small subset of Luau in Agda (#350) * First cut reading JSON into an Agda representation of Luau syntax 2022-02-09 08:26:58 +08:00			`module FFI.Data.Maybe where`

Prototyping strict mode (#399) * First cut of strict mode Co-authored-by: Lily Brown <lily@lily.fyi> 2022-03-03 06:02:51 +08:00			`open import Agda.Builtin.Equality using (_≡_; refl)`

Prototyping a small subset of Luau in Agda (#350) * First cut reading JSON into an Agda representation of Luau syntax 2022-02-09 08:26:58 +08: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) #-}`
Prototyping strict mode (#399) * First cut of strict mode Co-authored-by: Lily Brown <lily@lily.fyi> 2022-03-03 06:02:51 +08:00
			`just-inv : ∀ {A} {x y : A} → (just x ≡ just y) → (x ≡ y)`
			`just-inv refl = refl`