    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Bounded vectors
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Vec.Bounded where

    open import Level using (Level)
    open import Data.Nat.Base using (_≤_)
    open import Data.Vec.Base using (Vec)
    import Data.Vec as Vec using (filter; takeWhile; dropWhile)
    open import Function.Base using (id)
    open import Relation.Binary.Core using (_Preserves_⟶_)
    open import Relation.Unary using (Pred; Decidable)

    private
      variable
        a p : Level
        A : Set a

    ------------------------------------------------------------------------
    -- Publicly re-export the contents of the base module

    open import Data.Vec.Bounded.Base public

    ------------------------------------------------------------------------
    -- Additional operations

    lift : ∀ {f} → f Preserves _≤_ ⟶ _≤_ →
           (∀ {n} → Vec A n  → Vec≤ A (f n)) →
           ∀ {n} →  Vec≤ A n → Vec≤ A (f n)
    lift incr f (as , p) = ≤-cast (incr p) (f as)

    lift′ : (∀ {n} → Vec A n  → Vec≤ A n) →
            (∀ {n} → Vec≤ A n → Vec≤ A n)
    lift′ = lift id

    ------------------------------------------------------------------------
    -- Additional operations

    module _ {P : Pred A p} (P? : Decidable P) where

      filter : ∀ {n} → Vec≤ A n → Vec≤ A n
      filter = lift′ (Vec.filter P?)

      takeWhile : ∀ {n} → Vec≤ A n → Vec≤ A n
      takeWhile = lift′ (Vec.takeWhile P?)

      dropWhile : ∀ {n} → Vec≤ A n → Vec≤ A n
      dropWhile = lift′ (Vec.dropWhile P?)