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 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 aSource