Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered




currentProblem :: TCM ProblemIdSource

Get the current problem

stealConstraints :: ProblemId -> TCM ()Source

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

getAwakeConstraints :: TCM ConstraintsSource

Get the awake constraints

addConstraint' :: Constraint -> TCM ()Source

Add new a constraint

addAwakeConstraints :: Constraints -> TCM ()Source

Add already awake constraints

nowSolvingConstraints :: TCM a -> TCM aSource

Start solving constraints