------------------------------------------------------------------------
-- The Agda standard library
--
-- Permutation relations over Vector
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Functional.Relation.Binary.Permutation where
open import Level using (Level)
open import Data.Product.Base using (Σ-syntax)
open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_)
open import Data.Vec.Functional using (Vector)
open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
private
variable
a : Level
A : Set a
infix 3 _↭_
_↭_ : IRel (Vector A) _
xs ↭ ys = Σ[ ρ ∈ Permutation _ _ ] (∀ i → xs (ρ ⟨$⟩ʳ i) ≡ ys i)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4