module Agda.TypeChecking.Monad.Closure where

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Signature
import Agda.TypeChecking.Monad.Trace

enterClosure :: MonadTCM tcm => Closure a -> (a -> tcm b) -> tcm b
enterClosure (Closure sig env scope trace x) k =
    withScope_ scope
    $ withEnv env
    $ withTrace trace
    $ k x