------------------------------------------------------------------------ -- The Agda standard library -- -- Reflection utilities for List ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.List.Reflection where open import Data.List.Base open import Reflection.AST.Term open import Reflection.AST.Argument ------------------------------------------------------------------------ -- Type `List : Term → Term `List `A = def (quote List) (1 ⋯⟅∷⟆ `A ⟨∷⟩ []) ------------------------------------------------------------------------ -- Constructors `[] : Term `[] = con (quote List.[]) (2 ⋯⟅∷⟆ []) infixr 5 _`∷_ _`∷_ : Term → Term → Term x `∷ xs = con (quote List._∷_) (2 ⋯⟅∷⟆ x ⟨∷⟩ xs ⟨∷⟩ []) ------------------------------------------------------------------------ -- Patterns -- Can't be used on the RHS as the omitted args aren't inferable pattern `[]` = con (quote List.[]) _ pattern _`∷`_ x xs = con (quote List._∷_) (_ ∷ _ ∷ x ⟨∷⟩ xs ⟨∷⟩ _)