Source code on Github
{-# OPTIONS --safe --without-K #-}
module Reflection.Utils.Metas where

open import Meta.Prelude
open import Meta.Init

open import Data.List using (_++_)

isMeta : Term  Bool
isMeta = λ where
  (meta _ _)  true
  _           false

mutual
  findMetas : Term  List Term
  findMetas = λ where
    (var _ as)  findMetas* as
    (con _ as)  findMetas* as
    (def _ as)  findMetas* as
    (lam _ (abs _ x))  findMetas x
    (pat-lam cs as)    findMetasCl cs ++ findMetas* as
    (pi (arg _ a) (abs _ b))  findMetas a ++ findMetas b
    (agda-sort _)  []
    (lit _)        []
    m@(meta x as)  m  findMetas* as
    unknown        []

  findMetas* : List (Arg Term)  List Term
  findMetas* = λ where
    []  []
    ((arg _ t)  ts)  findMetas t ++ findMetas* ts

  findMetasCl : List Clause  List Term
  findMetasCl = λ where
    []  []
    (Clause.clause _ _ t  c)       findMetas t ++ findMetasCl c
    (Clause.absurd-clause _ _  c)  findMetasCl c