{-# OPTIONS --without-K --safe #-}
module Reflection.AST.Name where
open import Data.List.Base using (List)
import Data.Product.Properties as Prodₚ using (≡-dec)
import Data.Word64.Properties as Wₚ using (_≡?_)
open import Function.Base using (_on_)
open import Relation.Nullary.Decidable.Core using (map′)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
open import Relation.Binary.Construct.On using (decidable)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
open import Agda.Builtin.Reflection public
using (Name) renaming (primQNameToWord64s to toWords; primQNameEquality to _≡ᵇ_)
open import Agda.Builtin.Reflection.Properties public
renaming (primQNameToWord64sInjective to toWords-injective)
Names : Set
Names = List Name
infix 4 _≈?_ _≡?_ _≈_
_≈_ : Rel Name _
_≈_ = _≡_ on toWords
_≈?_ : Decidable _≈_
_≈?_ = decidable toWords _≡_ (Prodₚ.≡-dec Wₚ._≡?_ Wₚ._≡?_)
_≡?_ : DecidableEquality Name
m ≡? n = map′ (toWords-injective _ _) (cong toWords) (m ≈? n)
infix 4 _≟_
_≟_ = _≡?_
{-# WARNING_ON_USAGE _≟_
"Warning: _≟_ was deprecated in v2.4.
Please use _≡?_ instead."
#-}