Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 ConstraintsSource
Get the constraints
lookupConstraint :: MonadTCM tcm => Int -> tcm ConstraintClosureSource
takeConstraints :: MonadTCM tcm => tcm ConstraintsSource
Take constraints (clear all constraints).
withConstraint :: MonadTCM tcm => (Constraint -> tcm a) -> ConstraintClosure -> tcm aSource
addConstraints :: MonadTCM tcm => Constraints -> tcm ()Source
Add new constraints
buildConstraint :: MonadTCM tcm => Constraint -> tcm ConstraintsSource
Create a new constraint.
Produced by Haddock version 2.6.0