| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Monad.Constraints

Synopsis

getConstraints :: MonadTCM tcm => tcm Constraints
lookupConstraint :: MonadTCM tcm => Int -> tcm ConstraintClosure
takeConstraints :: MonadTCM tcm => tcm Constraints
withConstraint :: MonadTCM tcm => (Constraint -> tcm a) -> ConstraintClosure -> tcm a
addConstraints :: MonadTCM tcm => Constraints -> tcm ()
buildConstraint :: MonadTCM tcm => Constraint -> tcm Constraints

Documentation

getConstraints :: MonadTCM tcm => tcm Constraints | Source

Get the constraints

lookupConstraint :: MonadTCM tcm => Int -> tcm ConstraintClosure | Source

takeConstraints :: MonadTCM tcm => tcm Constraints | Source

Take constraints (clear all constraints).

withConstraint :: MonadTCM tcm => (Constraint -> tcm a) -> ConstraintClosure -> tcm a | Source

addConstraints :: MonadTCM tcm => Constraints -> tcm () | Source

Add new constraints

buildConstraint :: MonadTCM tcm => Constraint -> tcm Constraints | Source

Create a new constraint.
Produced by Haddock version 2.4.2