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

Agda.TypeChecking.Monad.Constraints

Synopsis

Documentation

getConstraints :: MonadTCM tcm => tcm Constraints

Get the constraints

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.