- catchConstraint :: MonadTCM tcm => Constraint -> TCM Constraints -> tcm Constraints
- addNewConstraints :: MonadTCM tcm => Constraints -> tcm ()
- noConstraints :: MonadTCM tcm => tcm Constraints -> tcm ()
- guardConstraint :: MonadTCM tcm => tcm Constraints -> Constraint -> tcm Constraints
- wakeupConstraints :: MonadTCM tcm => tcm ()
- solveConstraints :: MonadTCM tcm => Constraints -> tcm Constraints
- solveConstraint :: MonadTCM tcm => Constraint -> tcm Constraints
Documentation
catchConstraint :: MonadTCM tcm => Constraint -> TCM Constraints -> tcm ConstraintsSource
Catch pattern violation errors and adds a constraint.
addNewConstraints :: MonadTCM tcm => Constraints -> tcm ()Source
Try to solve the constraints to be added.
noConstraints :: MonadTCM tcm => tcm Constraints -> tcm ()Source
Don't allow the argument to produce any constraints.
guardConstraint :: MonadTCM tcm => tcm Constraints -> Constraint -> tcm ConstraintsSource
Guard constraint
wakeupConstraints :: MonadTCM tcm => tcm ()Source
We ignore the constraint ids and (as in Agda) retry all constraints every time. We probably generate very few constraints.
solveConstraints :: MonadTCM tcm => Constraints -> tcm ConstraintsSource
solveConstraint :: MonadTCM tcm => Constraint -> tcm ConstraintsSource