Agda-2.5.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Local

Synopsis

Documentation

makeLocal :: Free a => 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 => a -> TCM (Local a) Source #

getLocal :: Subst Term a => Local a -> TCM (Maybe a) Source #