------------------------------------------------------------------------
-- The Agda standard library
--
-- Patterns used in the reflection machinery
------------------------------------------------------------------------

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

module Reflection.AST.Pattern where

------------------------------------------------------------------------
-- Re-exporting the builtin type and constructors

open import Agda.Builtin.Reflection public using (Pattern)
open Pattern public

------------------------------------------------------------------------
-- Re-exporting definitions that used to be here

open import Reflection.AST.Term public
  using    ( proj-injective )
  renaming ( pat-con-injective₁ to con-injective₁
           ; pat-con-injective₂ to con-injective₂
           ; pat-con-injective  to con-injective
           ; pat-var-injective  to var-injective
           ; pat-lit-injective  to lit-injective
           ; _≟-Patterns_       to _≟s_
           ; _≟-Pattern_        to _≟_
           )