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

Safe HaskellNone

Agda.TypeChecking.Constraints

Synopsis

Documentation

catchConstraint :: Constraint -> TCM () -> TCM ()Source

Catches pattern violation errors and adds a constraint.

noConstraints :: TCM a -> TCM aSource

Don't allow the argument to produce any constraints.

newProblem :: TCM a -> TCM (ProblemId, a)Source

Create a fresh problem for the given action.

ifNoConstraints :: TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM bSource

ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM aSource

guardConstraint :: Constraint -> TCM () -> TCM ()Source

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.

whenConstraints :: TCM () -> TCM () -> TCM ()Source

wakeupConstraints :: MetaId -> TCM ()Source

Wake up the constraints depending on the given meta.

wakeupConstraints_ :: TCM ()Source

Wake up all constraints.