------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors where every pair of elements are related (symmetrically)
------------------------------------------------------------------------

-- Core modules are not meant to be used directly outside of the
-- standard library.

-- This module should be removable if and when Agda issue
-- https://github.com/agda/agda/issues/3210 is fixed

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

open import Relation.Binary.Core using (Rel)

module Data.Vec.Relation.Unary.AllPairs.Core
  {a } {A : Set a} (R : Rel A ) where

open import Level
open import Data.Vec.Base
open import Data.Vec.Relation.Unary.All

------------------------------------------------------------------------
-- Definition

-- AllPairs R xs means that every pair of elements (x , y) in xs is a
-- member of relation R (as long as x comes before y in the vector).

infixr 5 _∷_

data AllPairs :  {n}  Vec A n  Set (a  ) where
  []  : AllPairs []
  _∷_ :  {n x} {xs : Vec A n}  All (R x) xs  AllPairs xs  AllPairs (x  xs)