------------------------------------------------------------------------
-- 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 using (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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4