------------------------------------------------------------------------
-- The Agda standard library
--
-- Non-empty lists
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.List.NonEmpty where
 
open import Level using (Level)
open import Data.List.Base as List using (List)
 
------------------------------------------------------------------------
-- Re-export basic type and operations
 
open import Data.List.NonEmpty.Base public
 
 
------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
 
private
  variable
    a : Level
    A : Set a
 
-- Version 1.4
 
infixl  _∷ʳ'_
 
_∷ʳ'_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x)
_∷ʳ'_ = SnocView._∷ʳ′_
{-# WARNING_ON_USAGE _∷ʳ'_
"Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4.
Please use _∷ʳ′_ (ending in a prime) instead."
#-}