------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors
------------------------------------------------------------------------
-- This implementation is designed for reasoning about dynamic
-- vectors which may increase or decrease in size.
-- See `Data.Vec.Functional` for an alternative implementation as
-- functions from finite sets, which is more suitable for reasoning
-- about fixed sized vectors and for when ease of retrieval is
-- important.
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec where
open import Level
open import Data.Bool.Base
import Data.Nat.Properties as ℕ
open import Data.Vec.Bounded.Base as Vec≤
using (Vec≤; ≤-cast; fromVec)
open import Function.Base using (_$_)
open import Relation.Nullary
open import Relation.Unary
private
variable
a p : Level
A : Set a
------------------------------------------------------------------------
-- Publicly re-export the contents of the base module
open import Data.Vec.Base public
------------------------------------------------------------------------
-- Additional operations
module _ {P : A → Set p} (P? : Decidable P) where
filter : ∀ {n} → Vec A n → Vec≤ A n
filter [] = Vec≤.[]
filter (a ∷ as) = if does (P? a) then a Vec≤.∷_ else ≤-cast (ℕ.n≤1+n _) $ filter as
takeWhile : ∀ {n} → Vec A n → Vec≤ A n
takeWhile [] = Vec≤.[]
takeWhile (a ∷ as) = if does (P? a) then a Vec≤.∷ takeWhile as else Vec≤.[]
dropWhile : ∀ {n} → Vec A n → Vec≤ A n
dropWhile Vec.[] = Vec≤.[]
dropWhile (a Vec.∷ as) =
if does (P? a) then ≤-cast (ℕ.n≤1+n _) (dropWhile as)
else fromVec (a Vec.∷ as)
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