------------------------------------------------------------------------
-- The Agda standard library
--
-- The NonEmpty type which calls out to Haskell via the FFI
------------------------------------------------------------------------

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

module Foreign.Haskell.List.NonEmpty where

open import Level using (Level; _⊔_)
open import Data.List.NonEmpty.Base as Data using (_∷_)
open import Data.List using (List)

{-# FOREIGN GHC import qualified Data.List.NonEmpty as NE #-}

private
  variable
    a : Level
    A : Set a

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

data NonEmpty (A : Set a) : Set a where
  _∷_ : A → List A → NonEmpty A

infixr  _∷_

{-# FOREIGN GHC type AgdaNonEmpty l a = NE.NonEmpty a #-}
{-# COMPILE GHC NonEmpty = data AgdaNonEmpty ((NE.:|)) #-}