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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Constraints

Contents

Synopsis

Documentation

currentProblem :: TCM ProblemId #

Get the current problem

stealConstraints :: ProblemId -> TCM () #

Steal all constraints belonging to the given problem and add them to the current problem.

getAwakeConstraints :: TCM Constraints #

Get the awake constraints

holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a #

Suspend constraints matching the predicate during the execution of the second argument. Caution: held sleeping constraints will not be woken up by events that would normally trigger a wakeup call.

addConstraint' :: Constraint -> TCM () #

Add new a constraint

addAwakeConstraints :: Constraints -> TCM () #

Add already awake constraints

nowSolvingConstraints :: TCM a -> TCM a #

Start solving constraints

Lenses