------------------------------------------------------------------------
-- 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 _≟_
           )