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