------------------------------------------------------------------------
-- The Agda standard library
--
-- The reflected abstract syntax tree
------------------------------------------------------------------------

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

module Reflection.AST where

import Agda.Builtin.Reflection as Builtin

------------------------------------------------------------------------
-- Names, Metas, and Literals re-exported publicly

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

------------------------------------------------------------------------
-- Fixity

open Builtin public
  using (non-assoc; related; unrelated; fixity)
  renaming
  ( left-assoc      to assocˡ
  ; right-assoc     to assocʳ
  ; primQNameFixity to getFixity
  )