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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Monad.Sharing

Documentation

updateSharedTerm :: MonadTCM tcm => (Term -> tcm Term) -> Term -> tcm Term Source

updateSharedTermF :: (MonadTCM tcm, Traversable f) => (Term -> tcm (f Term)) -> Term -> tcm (f Term) Source

updateSharedTermT :: (MonadTCM tcm, MonadTrans t, Monad (t tcm)) => (Term -> t tcm Term) -> Term -> t tcm Term Source

forceEqualTerms :: Term -> Term -> TCM () Source

disableDestructiveUpdate :: TCM a -> TCM a Source