Agda.TypeChecking.Monad.Closure

Documentation

enterClosure :: (MonadTCEnv m, ReadTCState m, LensClosure a c) => c -> (a -> m b) -> m b

withClosure :: (MonadTCEnv m, ReadTCState m) => Closure a -> (a -> m b) -> m (Closure b)

mapClosure :: (MonadTCEnv m, ReadTCState m) => (a -> m b) -> Closure a -> m (Closure b)