------------------------------------------------------------------------
-- The Agda standard library
--
-- Instances for reflected syntax
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Reflection.AST.Instances where
open import Level
import Reflection.AST.Literal as Literal
import Reflection.AST.Name as Name
import Reflection.AST.Meta as Meta
import Reflection.AST.Abstraction as Abstraction
import Reflection.AST.Argument as Argument
import Reflection.AST.Argument.Visibility as Visibility
import Reflection.AST.Argument.Relevance as Relevance
import Reflection.AST.Argument.Quantity as Quantity
import Reflection.AST.Argument.Information as Information
import Reflection.AST.Pattern as Pattern
import Reflection.AST.Term as Term
open import Relation.Binary.PropositionalEquality.Core
open import Relation.Binary.PropositionalEquality.Properties
using (isDecEquivalence)
open import Relation.Binary.TypeClasses
private
variable
a : Level
A : Set a
instance
Lit-≡-isDecEquivalence = isDecEquivalence Literal._≟_
Name-≡-isDecEquivalence = isDecEquivalence Name._≟_
Meta-≡-isDecEquivalence = isDecEquivalence Meta._≟_
Visibility-≡-isDecEquivalence = isDecEquivalence Visibility._≟_
Relevance-≡-isDecEquivalence = isDecEquivalence Relevance._≟_
Quantity-≡-isDecEquivalence = isDecEquivalence Quantity._≟_
ArgInfo-≡-isDecEquivalence = isDecEquivalence Information._≟_
Pattern-≡-isDecEquivalence = isDecEquivalence Pattern._≟_
Clause-≡-isDecEquivalence = isDecEquivalence Term._≟-Clause_
Term-≡-isDecEquivalence = isDecEquivalence Term._≟_
Sort-≡-isDecEquivalence = isDecEquivalence Term._≟-Sort_
Abs-≡-isDecEquivalence : {{IsDecEquivalence {A = A} _≡_}} → IsDecEquivalence {A = Abstraction.Abs A} _≡_
Abs-≡-isDecEquivalence = isDecEquivalence (Abstraction.≡-dec _≟_)
Arg-≡-isDecEquivalence : {{IsDecEquivalence {A = A} _≡_}} → IsDecEquivalence {A = Argument.Arg A} _≡_
Arg-≡-isDecEquivalence = isDecEquivalence (Argument.≡-dec _≟_)
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