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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Monad.Constraints

Contents

Synopsis

Documentation

currentProblem :: TCM ProblemId Source

Get the current problem

stealConstraints :: ProblemId -> TCM () Source

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

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

isProblemSolved :: ProblemId -> TCM Bool Source

getConstraintsForProblem :: ProblemId -> TCM Constraints Source

getAwakeConstraints :: TCM Constraints Source

Get the awake constraints

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

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

putAllConstraintsToSleep :: TCM () Source

takeAwakeConstraint :: TCM (Maybe ProblemConstraint) Source

getAllConstraints :: TCM Constraints Source

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

buildProblemConstraint :: ProblemId -> Constraint -> TCM ProblemConstraint Source

buildConstraint :: Constraint -> TCM ProblemConstraint Source

addConstraint' :: Constraint -> TCM () Source

Add new a constraint

addAwakeConstraints :: Constraints -> TCM () Source

Add already awake constraints

nowSolvingConstraints :: TCM a -> TCM a Source

Start solving constraints

isSolvingConstraints :: TCM Bool Source

Lenses

mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState Source

mapSleepingConstraints :: (Constraints -> Constraints) -> TCState -> TCState Source

modifyAwakeConstraints :: (Constraints -> Constraints) -> TCM () Source

modifySleepingConstraints :: (Constraints -> Constraints) -> TCM () Source