module Agda.Interaction.InteractionTop where

import Agda.TypeChecking.Monad.Base (TCM)

showOpenMetas :: TCM [String]