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