------------------------------------------------------------------------
-- 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 _≟_
)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4