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

Agda.TypeChecking.Monad.Constraints

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

addConstraint' :: Constraint -> TCM ()

Add new a constraint

addAwakeConstraints :: Constraints -> TCM ()

Add already awake constraints

nowSolvingConstraints :: TCM a -> TCM a

Start solving constraints