------------------------------------------------------------------------
-- The Agda standard library
--
-- Non-empty lists where all elements satisfy a given property
------------------------------------------------------------------------

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

module Data.List.NonEmpty.Relation.Unary.All where

import Data.List.Relation.Unary.All as List
open import Data.List.Relation.Unary.All using ([]; _∷_)
open import Data.List.Base using ([]; _∷_)
open import Data.List.NonEmpty.Base using (List⁺; _∷_; toList)
open import Level
open import Relation.Unary using (Pred)

private
  variable
    a p : Level
    A : Set a
    P : Pred A p

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

-- Given a predicate P, then All P xs means that every element in xs
-- satisfies P. See `Relation.Unary` for an explanation of predicates.

infixr 5 _∷_

data All {A : Set a} (P : Pred A p) : Pred (List⁺ A) (a  p) where
  _∷_ :  {x xs} (px : P x) (pxs : List.All P xs)  All P (x  xs)

------------------------------------------------------------------------
-- Functions

toList⁺ :  {xs : List⁺ A}  All P xs  List.All P (toList xs)
toList⁺ (px  pxs) = px  pxs