ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Constraints
Synopsis
- value addConstraintTCM
- value wakeConstraintsTCM
- value stealConstraintsTCM
- value noConstraints
- value reallyNoConstraints
- value noConstraints'
- value nonConstraining
- value newProblem
- value newProblem_
- value ifNoConstraints
- value ifNoConstraints_
- value guardConstraint
- value whenConstraints
- value wakeupConstraints
- value wakeupConstraints_
- value solveSomeAwakeConstraintsTCM
- value solveConstraintTCM
- value solveConstraint_
- value checkTypeCheckingProblem
- value debugConstraints
- value updateBlocker
- value addAndUnblocker
- value addOrUnblocker
- value withReduced
- PackageAgda-2.8.0.2
- Exports24
- LanguageHaskell2010
- LicenceMIT
- SourceConstraints.hs
Add all constraints belonging to the given problem to the current problem(s).
Don't allow the argument to produce any blocking constraints.
WARNING: this does not mean that the given computation cannot constrain the solution space further. It can well do so, by solving metas.
As noConstraints but also fail for non-blocking constraints.
Run a computation that should succeeds without constraining the solution space, i.e., not add any information about meta-variables.
Create a fresh problem for the given action.
guardConstraint c blocker tries to solve blocker first.
If successful without constraints, it moves on to solve c, otherwise it
adds a c to the constraint pool, blocked by the problem generated by blocker.
Wake up the constraints depending on the given meta.
Wake up all constraints not blocked on a problem.
Solve awake constraints matching the predicate. If the second argument is True solve constraints even if already isSolvingConstraints.