------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of fresh lists and functions acting on them
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Fresh.Properties where
open import Data.List.Fresh using (List#; _∷#_; _#_; Empty; NonEmpty; cons; [])
open import Data.Product.Base using (_,_)
open import Level using (Level; _⊔_)
open import Relation.Nullary.Decidable using (Dec; yes; no)
open import Relation.Nullary.Negation using (¬_)
open import Relation.Unary as U using (Pred)
import Relation.Binary.Definitions as B using (_Respectsˡ_; Irrelevant)
open import Relation.Binary.Core using (Rel)
private
variable
a b e p r : Level
A : Set a
B : Set b
------------------------------------------------------------------------
-- Fresh congruence
module _ {R : Rel A r} {_≈_ : Rel A e} (R≈ : R B.Respectsˡ _≈_) where
fresh-respectsˡ : ∀ {x y} {xs : List# A R} → x ≈ y → x # xs → y # xs
fresh-respectsˡ {xs = []} x≈y x#xs = _
fresh-respectsˡ {xs = x ∷# xs} x≈y (r , x#xs) =
R≈ x≈y r , fresh-respectsˡ x≈y x#xs
------------------------------------------------------------------------
-- Empty and NotEmpty
Empty⇒¬NonEmpty : {R : Rel A r} {xs : List# A R} → Empty xs → ¬ (NonEmpty xs)
Empty⇒¬NonEmpty [] ()
NonEmpty⇒¬Empty : {R : Rel A r} {xs : List# A R} → NonEmpty xs → ¬ (Empty xs)
NonEmpty⇒¬Empty () []
empty? : {R : Rel A r} (xs : List# A R) → Dec (Empty xs)
empty? [] = yes []
empty? (_ ∷# _) = no (λ ())
nonEmpty? : {R : Rel A r} (xs : List# A R) → Dec (NonEmpty xs)
nonEmpty? [] = no (λ ())
nonEmpty? (cons x xs pr) = yes (cons x xs pr)
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