------------------------------------------------------------------------
-- The Agda standard library
--
-- Reflection utilities
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Reflection.TCM.Utilities where
open import Data.List using (List; []; _∷_; _++_; map)
open import Data.Unit using (⊤; tt)
open import Effect.Applicative using (RawApplicative; mkRawApplicative)
open import Function.Base using (case_of_)
open import Reflection.AST.Meta using (Meta)
open import Reflection.AST.Term using (Term)
open import Reflection.TCM using (TC; pure; blockTC; blockerAll; blockerMeta)
import Reflection.AST.Traversal as Traversal
blockOnMetas : Term → TC ⊤
blockOnMetas t =
case traverseTerm actions (0 , []) t of λ where
[] → pure tt
xs@(_ ∷ _) → blockTC (blockerAll (map blockerMeta xs))
where
applicative : ∀ {ℓ} → RawApplicative {ℓ} (λ _ → List Meta)
applicative = mkRawApplicative (λ _ → List Meta) (λ _ → []) _++_
open Traversal applicative
actions : Actions
actions = record defaultActions { onMeta = λ _ x → x ∷ [] }
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