Source code on Github
{-# OPTIONS --cubical-compatible --safe #-}
module Reflection where
import Agda.Builtin.Reflection as Builtin
open import Reflection.Abstraction as Abstraction public
using (Abs; abs)
open import Reflection.Argument as Argument public
using (Arg; arg; Args; vArg; hArg; iArg; defaultModality)
open import Reflection.Definition as Definition public
using (Definition)
open import Reflection.Meta as Meta public
using (Meta)
open import Reflection.Name as Name public
using (Name; Names)
open import Reflection.Literal as Literal public
using (Literal)
open import Reflection.Pattern as Pattern public
using (Pattern)
open import Reflection.Term as Term public
using (Term; Type; Clause; Clauses; Sort)
import Reflection.Argument.Modality as Modality
import Reflection.Argument.Quantity as Quantity
import Reflection.Argument.Relevance as Relevance
import Reflection.Argument.Visibility as Visibility
import Reflection.Argument.Information as Information
open Definition.Definition public
open Information.ArgInfo public
open Literal.Literal public
open Modality.Modality public
open Quantity.Quantity public
open Relevance.Relevance public
open Term.Term public
open Visibility.Visibility public
open Builtin public
using (non-assoc; related; unrelated; fixity)
renaming
( left-assoc to assocˡ
; right-assoc to assocʳ
; primQNameFixity to getFixity
)
open import Reflection.TypeChecking.Monad public
open import Reflection.TypeChecking.Monad.Syntax public
using (_>>=_; _>>_)
open import Reflection.Show public
returnTC = return
{-# WARNING_ON_USAGE returnTC
"Warning: returnTC was deprecated in v1.1.
Please use return instead."
#-}
Arg-info = Information.ArgInfo
{-# WARNING_ON_USAGE Arg-info
"Warning: Arg-info was deprecated in v1.3.
Please use Reflection.Argument.Information's ArgInfo instead."
#-}
infix 4 _≟-Lit_ _≟-Name_ _≟-Meta_ _≟-Visibility_ _≟-Relevance_ _≟-Arg-info_
_≟-Pattern_ _≟-ArgPatterns_
_≟-Lit_ = Literal._≟_
{-# WARNING_ON_USAGE _≟-Lit_
"Warning: _≟-Lit_ was deprecated in v1.3.
Please use Reflection.Literal's _≟_ instead."
#-}
_≟-Name_ = Name._≟_
{-# WARNING_ON_USAGE _≟-Name_
"Warning: _≟-Name_ was deprecated in v1.3.
Please use Reflection.Name's _≟_ instead."
#-}
_≟-Meta_ = Meta._≟_
{-# WARNING_ON_USAGE _≟-Meta_
"Warning: _≟-Meta_ was deprecated in v1.3.
Please use Reflection.Meta's _≟_ instead."
#-}
_≟-Visibility_ = Visibility._≟_
{-# WARNING_ON_USAGE _≟-Visibility_
"Warning: _≟-Visibility_ was deprecated in v1.3.
Please use Reflection.Argument.Visibility's _≟_ instead."
#-}
_≟-Relevance_ = Relevance._≟_
{-# WARNING_ON_USAGE _≟-Relevance_
"Warning: _≟-Relevance_ was deprecated in v1.3.
Please use Reflection.Argument.Relevance's _≟_ instead."
#-}
_≟-Arg-info_ = Information._≟_
{-# WARNING_ON_USAGE _≟-Arg-info_
"Warning: _≟-Arg-info_ was deprecated in v1.3.
Please use Reflection.Argument.Information's _≟_ instead."
#-}
_≟-Pattern_ = Pattern._≟_
{-# WARNING_ON_USAGE _≟-Pattern_
"Warning: _≟-Pattern_ was deprecated in v1.3.
Please use Reflection.Pattern's _≟_ instead."
#-}
_≟-ArgPatterns_ = Pattern._≟s_
{-# WARNING_ON_USAGE _≟-ArgPatterns_
"Warning: _≟-ArgPatterns_ was deprecated in v1.3.
Please use Reflection.Pattern's _≟s_ instead."
#-}
map-Abs = Abstraction.map
{-# WARNING_ON_USAGE map-Abs
"Warning: map-Abs was deprecated in v1.3.
Please use Reflection.Abstraction's map instead."
#-}
map-Arg = Argument.map
{-# WARNING_ON_USAGE map-Arg
"Warning: map-Arg was deprecated in v1.3.
Please use Reflection.Argument's map instead."
#-}
map-Args = Argument.map-Args
{-# WARNING_ON_USAGE map-Args
"Warning: map-Args was deprecated in v1.3.
Please use Reflection.Argument's map-Args instead."
#-}
visibility = Information.visibility
{-# WARNING_ON_USAGE visibility
"Warning: visibility was deprecated in v1.3.
Please use Reflection.Argument.Information's visibility instead."
#-}
relevance = Modality.relevance
{-# WARNING_ON_USAGE relevance
"Warning: relevance was deprecated in v1.3.
Please use Reflection.Argument.Modality's relevance instead."
#-}
infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_
_≟-Clause_ _≟-Clauses_ _≟_
_≟-Sort_
_≟-AbsTerm_ = Term._≟-AbsTerm_
{-# WARNING_ON_USAGE _≟-AbsTerm_
"Warning: _≟-AbsTerm_ was deprecated in v1.3.
Please use Reflection.Term's _≟-AbsTerm_ instead."
#-}
_≟-AbsType_ = Term._≟-AbsType_
{-# WARNING_ON_USAGE _≟-AbsType_
"Warning: _≟-AbsType_ was deprecated in v1.3.
Please use Reflection.Term's _≟-AbsType_ instead."
#-}
_≟-ArgTerm_ = Term._≟-ArgTerm_
{-# WARNING_ON_USAGE _≟-ArgTerm_
"Warning: _≟-ArgTerm_ was deprecated in v1.3.
Please use Reflection.Term's _≟-ArgTerm_ instead."
#-}
_≟-ArgType_ = Term._≟-ArgType_
{-# WARNING_ON_USAGE _≟-ArgType_
"Warning: _≟-ArgType_ was deprecated in v1.3.
Please use Reflection.Term's _≟-ArgType_ instead."
#-}
_≟-Args_ = Term._≟-Args_
{-# WARNING_ON_USAGE _≟-Args_
"Warning: _≟-Args_ was deprecated in v1.3.
Please use Reflection.Term's _≟-Args_ instead."
#-}
_≟-Clause_ = Term._≟-Clause_
{-# WARNING_ON_USAGE _≟-Clause_
"Warning: _≟-Clause_ was deprecated in v1.3.
Please use Reflection.Term's _≟-Clause_ instead."
#-}
_≟-Clauses_ = Term._≟-Clauses_
{-# WARNING_ON_USAGE _≟-Clauses_
"Warning: _≟-Clauses_ was deprecated in v1.3.
Please use Reflection.Term's _≟-Clauses_ instead."
#-}
_≟_ = Term._≟_
{-# WARNING_ON_USAGE _≟_
"Warning: _≟_ was deprecated in v1.3.
Please use Reflection.Term's _≟_ instead."
#-}
_≟-Sort_ = Term._≟-Sort_
{-# WARNING_ON_USAGE _≟-Sort_
"Warning: _≟-Sort_ was deprecated in v1.3.
Please use Reflection.Term's _≟-Sort_ instead."
#-}