Agda.TypeChecking.Monad.Constraints
- getConstraints :: MonadTCM tcm => tcm Constraints
- lookupConstraint :: MonadTCM tcm => Int -> tcm ConstraintClosure
- takeConstraints :: MonadTCM tcm => tcm Constraints
- withConstraint :: MonadTCM tcm => (Constraint -> tcm a) -> ConstraintClosure -> tcm a
- addConstraints :: MonadTCM tcm => Constraints -> tcm ()
- buildConstraint :: MonadTCM tcm => Constraint -> tcm Constraints
Documentation
getConstraints :: MonadTCM tcm => tcm Constraints
Get the constraints
lookupConstraint :: MonadTCM tcm => Int -> tcm ConstraintClosure
takeConstraints :: MonadTCM tcm => tcm Constraints
Take constraints (clear all constraints).
withConstraint :: MonadTCM tcm => (Constraint -> tcm a) -> ConstraintClosure -> tcm a
addConstraints :: MonadTCM tcm => Constraints -> tcm ()
Add new constraints
buildConstraint :: MonadTCM tcm => Constraint -> tcm Constraints
Create a new constraint.