------------------------------------------------------------------------
-- The Agda standard library
--
-- Metavariables used in the reflection machinery
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Reflection.AST.Meta where

import Data.Nat.Properties as ℕ 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)
import Relation.Binary.Construct.On as On using (decidable)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)

open import Agda.Builtin.Reflection public
  using (Meta) renaming (primMetaToNat to toℕ; primMetaEquality to _≡ᵇ_)

open import Agda.Builtin.Reflection.Properties public
  renaming (primMetaToNatInjective to toℕ-injective)

-- Equality of metas is decidable.

infix  _≈?_ _≡?_ _≈_

_≈_ : Rel Meta _
_≈_ = _≡_ on toℕ

_≈?_ : Decidable _≈_
_≈?_ = On.decidable toℕ _≡_ ℕ._≡?_

_≡?_ : DecidableEquality Meta
m ≡? n = map′ (toℕ-injective _ _) (cong toℕ) (m ≈? n)


------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.4

infix  _≟_
_≟_ = _≡?_
{-# WARNING_ON_USAGE _≟_
"Warning: _≟_ was deprecated in v2.4.
Please use _≡?_ instead."
#-}