Safe Haskell | None |
---|
Agda.TypeChecking.Constraints
- catchConstraint :: Constraint -> TCM () -> TCM ()
- addConstraint :: Constraint -> TCM ()
- noConstraints :: TCM a -> TCM a
- newProblem :: TCM a -> TCM (ProblemId, a)
- newProblem_ :: TCM () -> TCM ProblemId
- ifNoConstraints :: TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
- ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
- guardConstraint :: Constraint -> TCM () -> TCM ()
- whenConstraints :: TCM () -> TCM () -> TCM ()
- wakeupConstraints :: MetaId -> TCM ()
- wakeupConstraints_ :: TCM ()
- solveAwakeConstraints :: TCM ()
- solveAwakeConstraints' :: Bool -> TCM ()
- solveConstraint :: Constraint -> TCM ()
- solveConstraint_ :: Constraint -> TCM ()
Documentation
catchConstraint :: Constraint -> TCM () -> TCM ()
Catches pattern violation errors and adds a constraint.
addConstraint :: Constraint -> TCM ()
noConstraints :: TCM a -> TCM a
Don't allow the argument to produce any constraints.
newProblem :: TCM a -> TCM (ProblemId, a)
Create a fresh problem for the given action.
newProblem_ :: TCM () -> TCM ProblemId
guardConstraint :: Constraint -> TCM () -> TCM ()
guardConstraint c blocker
tries to solve blocker
first.
If successful without constraints, it moves on to solve c
, otherwise it
adds a Guarded c cs
constraint
to the blocker
-generated constraints cs
.
wakeupConstraints :: MetaId -> TCM ()
Wake up the constraints depending on the given meta.
Wake up all constraints.
solveAwakeConstraints' :: Bool -> TCM ()
solveConstraint :: Constraint -> TCM ()
solveConstraint_ :: Constraint -> TCM ()