------------------------------------------------------------------------ -- The Agda standard library -- -- Lists 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.List.Relation.Unary.AllPairs.Core {a ℓ} {A : Set a} (R : Rel A ℓ) where open import Level open import Data.List.Base open import Data.List.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 list). infixr 5 _∷_ data AllPairs : List A → Set (a ⊔ ℓ) where [] : AllPairs [] _∷_ : ∀ {x xs} → All (R x) xs → AllPairs xs → AllPairs (x ∷ xs)