------------------------------------------------------------------------
-- The Agda standard library
--
-- Argument visibility used in the reflection machinery
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Reflection.AST.Argument.Visibility where

open import Relation.Nullary.Decidable.Core            using (yes; no)
open import Relation.Binary.Definitions                using (DecidableEquality)
open import Relation.Binary.PropositionalEquality.Core using (refl)

------------------------------------------------------------------------
-- Re-exporting the builtins publicly

open import Agda.Builtin.Reflection public using (Visibility)
open Visibility public

------------------------------------------------------------------------
-- Decidable equality

infix 4 _≟_

_≟_ : DecidableEquality Visibility
visible    visible   = yes refl
hidden     hidden    = yes refl
instance′  instance′ = yes refl
visible    hidden    = no λ()
visible    instance′ = no λ()
hidden     visible   = no λ()
hidden     instance′ = no λ()
instance′  visible   = no λ()
instance′  hidden    = no λ()