summaryrefslogtreecommitdiff
path: root/src/full/Agda/Interaction/InteractionTop.hs-boot
blob: 41d5e1ea0b886764e1fcaae9a32a0e15eeef5193 (plain)
1
2
3
4
5
module Agda.Interaction.InteractionTop where

import Agda.TypeChecking.Monad.Base (TCM)

showOpenMetas :: TCM [String]