------------------------------------------------------------------------
-- The Agda standard library
--
-- Metavariables used in the reflection machinery
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --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 4 _≈?_ _≟_ _≈_
_≈_ : Rel Meta _
_≈_ = _≡_ on toℕ
_≈?_ : Decidable _≈_
_≈?_ = On.decidable toℕ _≡_ ℕ._≟_
_≟_ : DecidableEquality Meta
m ≟ n = map′ (toℕ-injective _ _) (cong toℕ) (m ≈? n)
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