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

Safe Haskell | None

Agda.TypeChecking.Monad.Constraints

Synopsis

- currentProblem :: TCM ProblemId
- stealConstraints :: ProblemId -> TCM ()
- solvingProblem :: ProblemId -> TCM a -> TCM a
- isProblemSolved :: ProblemId -> TCM Bool
- getConstraintsForProblem :: ProblemId -> TCM Constraints
- getAwakeConstraints :: TCM Constraints
- wakeConstraints :: (ProblemConstraint -> Bool) -> TCM ()
- dropConstraints :: (ProblemConstraint -> Bool) -> TCM ()
- putAllConstraintsToSleep :: TCM ()
- takeAwakeConstraint :: TCM (Maybe ProblemConstraint)
- getAllConstraints :: TCM Constraints
- withConstraint :: (Constraint -> TCM a) -> ProblemConstraint -> TCM a
- buildProblemConstraint :: ProblemId -> Constraint -> TCM ProblemConstraint
- buildConstraint :: Constraint -> TCM ProblemConstraint
- addConstraint' :: Constraint -> TCM ()
- addAwakeConstraints :: Constraints -> TCM ()
- nowSolvingConstraints :: TCM a -> TCM a
- isSolvingConstraints :: TCM Bool

# 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.

solvingProblem :: ProblemId -> TCM a -> TCM a

isProblemSolved :: ProblemId -> TCM Bool

getConstraintsForProblem :: ProblemId -> TCM Constraints

getAwakeConstraints :: TCM Constraints

Get the awake constraints

wakeConstraints :: (ProblemConstraint -> Bool) -> TCM ()

dropConstraints :: (ProblemConstraint -> Bool) -> TCM ()

putAllConstraintsToSleep :: TCM ()

takeAwakeConstraint :: TCM (Maybe ProblemConstraint)

getAllConstraints :: TCM Constraints

withConstraint :: (Constraint -> TCM a) -> ProblemConstraint -> TCM a

buildProblemConstraint :: ProblemId -> Constraint -> TCM ProblemConstraint

buildConstraint :: Constraint -> TCM ProblemConstraint

addConstraint' :: Constraint -> TCM ()

Add new a constraint

addAwakeConstraints :: Constraints -> TCM ()

Add already awake constraints

nowSolvingConstraints :: TCM a -> TCM a

Start solving constraints

isSolvingConstraints :: TCM Bool