------------------------------------------------------------------------
-- The Agda standard library
--
-- Streams where at least one element satisfies a given property
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible --guardedness #-}
module Codata.Guarded.Stream.Relation.Unary.Any where
open import Codata.Guarded.Stream as Stream using (Stream)
open import Data.Nat.Base hiding (_⊔_)
open import Level hiding (zero; suc)
open import Relation.Nullary.Negation.Core using (¬_; contradiction)
open import Relation.Unary using (Pred; _⊆_)
private
variable
a p q : Level
A : Set a
P Q : Pred A p
xs : Stream A
data Any {A : Set a} (P : Pred A p) : Stream A → Set (a ⊔ p) where
here : ∀ {xs} → P (Stream.head xs) → Any P xs
there : ∀ {xs} → Any P (Stream.tail xs) → Any P xs
head : ¬ Any P (Stream.tail xs) → Any P xs → P (Stream.head xs)
head ¬t (here h) = h
head ¬t (there t) = contradiction t ¬t
tail : ¬ P (Stream.head xs) → Any P xs → Any P (Stream.tail xs)
tail ¬h (here h) = contradiction h ¬h
tail ¬h (there t) = t
map : P ⊆ Q → Any P ⊆ Any Q
map g (here px ) = here (g px)
map g (there pxs) = there (map g pxs)
index : Any P xs → ℕ
index (here px ) = zero
index (there pxs) = suc (index pxs)
lookup : {P : Pred A p} → Any P xs → A
lookup {xs = xs} p = Stream.lookup xs (index p)
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