123456789101112131415161718192021222324252627282930-------------------------------------------------------------------------- The Agda standard library---- Argument relevance used in the reflection machinery------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Reflection.AST.Argument.Relevance 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 (Relevance)open Relevance public -------------------------------------------------------------------------- Decidable equality infix 4 _≟_ _≟_ : DecidableEquality Relevancerelevant ≟ relevant = yes reflirrelevant ≟ irrelevant = yes reflrelevant ≟ irrelevant = no λ()irrelevant ≟ relevant = no λ()