------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED.
--
-- Please use Data.Vec.Relation.Pointwise.Inductive
-- and Data.Vec.Relation.Pointwise.Extensional directly.
------------------------------------------------------------------------

module Relation.Binary.Vec.Pointwise where

open import Data.Vec.Relation.Pointwise.Inductive public
  hiding (head; tail)
open import Data.Vec.Relation.Pointwise.Extensional public
  using (head; tail) renaming (Pointwise to Pointwise′)