AgdaInternals

Missing instances for WriterT in Agda's internals.

NB: we are not exporting any definitions, just typeclass instances.

Orphan instances

(Monoid r, MonadFresh i m) => MonadFresh i (WriterT r m)

Methods

fresh :: WriterT r m i

(Monoid r, MonadBlock m) => MonadBlock (WriterT r m)

Methods

patternViolation :: Blocker -> WriterT r m a

catchPatternErr :: (Blocker -> WriterT r m a) -> WriterT r m a -> WriterT r m a

(Monoid r, MonadStConcreteNames m) => MonadStConcreteNames (WriterT r m)

Methods

runStConcreteNames :: StateT ConcreteNames (WriterT r m) a -> WriterT r m a

useConcreteNames :: WriterT r m ConcreteNames

modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> WriterT r m ()

(Monoid r, MonadTCM m, MonadConstraint m) => MonadConstraint (WriterT r m)

Methods

addConstraint :: Blocker -> Constraint -> WriterT r m ()

addAwakeConstraint :: Blocker -> Constraint -> WriterT r m ()

solveConstraint :: Constraint -> WriterT r m ()

solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> WriterT r m ()

wakeConstraints :: (ProblemConstraint -> WakeUp) -> WriterT r m ()

stealConstraints :: ProblemId -> WriterT r m ()

modifyAwakeConstraints :: (Constraints -> Constraints) -> WriterT r m ()

modifySleepingConstraints :: (Constraints -> Constraints) -> WriterT r m ()

(Monoid r, MonadInteractionPoints m) => MonadInteractionPoints (WriterT r m)

Methods

freshInteractionId :: WriterT r m InteractionId

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> WriterT r m ()

(Monoid r, MonadTCM m, MonadMetaSolver m) => MonadMetaSolver (WriterT r m)

Methods

newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> WriterT r m MetaId

assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> WriterT r m ()

assignTerm' :: MetaId -> [Arg ArgName] -> Term -> WriterT r m ()

etaExpandMeta :: [MetaKind] -> MetaId -> WriterT r m ()

updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> WriterT r m ()

speculateMetas :: WriterT r m () -> WriterT r m KeepMetas -> WriterT r m ()

(Monoid r, MonadWarning m) => MonadWarning (WriterT r m)

Methods

addWarning :: TCWarning -> WriterT r m ()

(Monoid r, Monad m, IsString (m a)) => IsString (WriterT r m a)

Methods

fromString :: String -> WriterT r m a

(Monoid r, Monad m, Semigroup (m Doc)) => Semigroup (WriterT r m Doc)

Methods

(<>) :: WriterT r m Doc -> WriterT r m Doc -> WriterT r m Doc

sconcat :: NonEmpty (WriterT r m Doc) -> WriterT r m Doc

stimes :: Integral b => b -> WriterT r m Doc -> WriterT r m Doc