------------------------------------------------------------------------
-- The Agda standard library
--
-- Vector equality over propositional equality
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Relation.Binary.Equality.Propositional {a} {A : Set a} where
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Vec.Base using (Vec)
open import Data.Vec.Relation.Binary.Pointwise.Inductive
using (Pointwise-≡⇒≡; ≡⇒Pointwise-≡)
import Data.Vec.Relation.Binary.Equality.Setoid as SEq
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
open import Relation.Binary.PropositionalEquality.Properties using (setoid)
------------------------------------------------------------------------
-- Publically re-export everything from setoid equality
open SEq (setoid A) public
------------------------------------------------------------------------
-- ≋ is propositional
≋⇒≡ : ∀ {n} {xs ys : Vec A n} → xs ≋ ys → xs ≡ ys
≋⇒≡ = Pointwise-≡⇒≡
≡⇒≋ : ∀ {n} {xs ys : Vec A n} → xs ≡ ys → xs ≋ ys
≡⇒≋ = ≡⇒Pointwise-≡
-- See also Data.Vec.Relation.Binary.Equality.Propositional.WithK.≋⇒≅.
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