Agda-2.5.2: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.Monad.Local
Synopsis
makeLocal :: Free' a All => a -> TCM (Local a) Source #
Precondition: must not be called if the module parameter of the current module have been refined or (touched at all).
makeGlobal :: Free' a All => a -> TCM (Local a) Source #
getLocal :: Subst Term a => Local a -> TCM (Maybe a) Source #