Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Constraints

Synopsis

Documentation

stealConstraintsTCM :: ProblemId -> TCM () Source #

Add all constraints belonging to the given problem to the current problem(s).

noConstraints :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m) => m a -> m a Source #

Don't allow the argument to produce any blocking constraints.

newProblem :: (MonadFresh ProblemId m, MonadConstraint m) => m a -> m (ProblemId, a) Source #

Create a fresh problem for the given action.

ifNoConstraints :: TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b Source #

ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a Source #

guardConstraint :: Constraint -> TCM () -> TCM () Source #

guardConstraint c blocker tries to solve blocker first. If successful without constraints, it moves on to solve c, otherwise it adds a Guarded c cs constraint to the blocker-generated constraints cs.

whenConstraints :: TCM () -> TCM () -> TCM () Source #

wakeConstraints' :: (ProblemConstraint -> TCM Bool) -> TCM () Source #

Wake constraints matching the given predicate (and aren't instance constraints if shouldPostponeInstanceSearch).

wakeupConstraints :: MetaId -> TCM () Source #

Wake up the constraints depending on the given meta.

wakeupConstraints_ :: TCM () Source #

Wake up all constraints.

solveSomeAwakeConstraintsTCM :: (ProblemConstraint -> Bool) -> Bool -> TCM () Source #

Solve awake constraints matching the predicate. If the second argument is True solve constraints even if already isSolvingConstraints.

Orphan instances