------------------------------------------------------------------------
-- The Agda standard library
--
-- Argument information used in the reflection machinery
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Reflection.AST.Argument.Information where
open import Data.Product.Base using (_×_; <_,_>; uncurry)
open import Relation.Nullary.Decidable.Core using (map′; _×-dec_)
open import Relation.Binary.Definitions using (DecidableEquality)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
open import Reflection.AST.Argument.Modality as Modality using (Modality)
open import Reflection.AST.Argument.Visibility as Visibility using (Visibility)
private
variable
v v′ : Visibility
m m′ : Modality
------------------------------------------------------------------------
-- Re-exporting the builtins publicly
open import Agda.Builtin.Reflection public using (ArgInfo)
open ArgInfo public
------------------------------------------------------------------------
-- Operations
visibility : ArgInfo → Visibility
visibility (arg-info v _) = v
modality : ArgInfo → Modality
modality (arg-info _ m) = m
------------------------------------------------------------------------
-- Decidable equality
arg-info-injective₁ : arg-info v m ≡ arg-info v′ m′ → v ≡ v′
arg-info-injective₁ refl = refl
arg-info-injective₂ : arg-info v m ≡ arg-info v′ m′ → m ≡ m′
arg-info-injective₂ refl = refl
arg-info-injective : arg-info v m ≡ arg-info v′ m′ → v ≡ v′ × m ≡ m′
arg-info-injective = < arg-info-injective₁ , arg-info-injective₂ >
infix 4 _≟_
_≟_ : DecidableEquality ArgInfo
arg-info v m ≟ arg-info v′ m′ =
map′
(uncurry (cong₂ arg-info))
arg-info-injective
(v Visibility.≟ v′ ×-dec m Modality.≟ m′)
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