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

Safe Haskell | None

Agda.TypeChecking.Monad.Sharing

# Documentation

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

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

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

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

disableDestructiveUpdate :: TCM a -> TCM a