{-# OPTIONS --cubical-compatible --safe #-}
module Reflection.AST where
import Agda.Builtin.Reflection as Builtin
open import Reflection.AST.Abstraction as Abstraction public
using (Abs; abs)
open import Reflection.AST.Argument as Argument public
using (Arg; arg; Args; vArg; hArg; iArg; defaultModality)
open import Reflection.AST.Definition as Definition public
using (Definition)
open import Reflection.AST.Meta as Meta public
using (Meta)
open import Reflection.AST.Name as Name public
using (Name; Names)
open import Reflection.AST.Literal as Literal public
using (Literal)
open import Reflection.AST.Pattern as Pattern public
using (Pattern)
open import Reflection.AST.Term as Term public
using (Term; Type; Clause; Clauses; Sort)
import Reflection.AST.Argument.Modality as Modality
import Reflection.AST.Argument.Quantity as Quantity
import Reflection.AST.Argument.Relevance as Relevance
import Reflection.AST.Argument.Visibility as Visibility
import Reflection.AST.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 import Reflection.AST.Show public
open Builtin public
using (non-assoc; related; unrelated; fixity)
renaming
( left-assoc to assocˡ
; right-assoc to assocʳ
; primQNameFixity to getFixity
)