------------------------------------------------------------------------ -- The Agda standard library -- -- This module is DEPRECATED. Please use -- Data.Vec.Relation.Binary.Pointwise.Extensional directly. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Data.Vec.Relation.Pointwise.Extensional where open import Data.Vec.Relation.Binary.Pointwise.Extensional public