------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of All predicate transformer for fresh lists
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Fresh.Relation.Unary.All.Properties where
open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
open import Data.List.Fresh.Relation.Unary.All using (All; []; _∷_; append)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Product.Base using (_,_)
open import Function.Base using (_∘′_)
open import Level using (Level; _⊔_; Lift)
open import Relation.Unary as U using (Pred)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
private
variable
a p r : Level
A : Set a
module _ {R : Rel A r} where
fromAll : ∀ {x} {xs : List# A R} → All (R x) xs → x # xs
fromAll [] = _
fromAll (p ∷ ps) = p , fromAll ps
toAll : ∀ {x} {xs : List# A R} → x # xs → All (R x) xs
toAll {xs = []} _ = []
toAll {xs = a ∷# as} (p , ps) = p ∷ toAll ps
module _ {R : Rel A r} {P : Pred A p} where
append⁺ : {xs ys : List# A R} {ps : All (_# ys) xs} →
All P xs → All P ys → All P (append xs ys ps)
append⁺ [] pys = pys
append⁺ (px ∷ pxs) pys = px ∷ append⁺ pxs pys
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