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

Agda.TypeChecking.Constraints

Synopsis

catchConstraint :: MonadTCM tcm => Constraint -> TCM Constraints -> tcm Constraints
addNewConstraints :: MonadTCM tcm => Constraints -> tcm ()
noConstraints :: MonadTCM tcm => tcm Constraints -> tcm ()
guardConstraint :: MonadTCM tcm => tcm Constraints -> Constraint -> tcm Constraints
wakeupConstraints :: MonadTCM tcm => tcm ()
solveConstraints :: MonadTCM tcm => Constraints -> tcm Constraints
solveConstraint :: MonadTCM tcm => Constraint -> tcm Constraints

Documentation

catchConstraint :: MonadTCM tcm => Constraint -> TCM Constraints -> tcm Constraints | Source

Catch pattern violation errors and adds a constraint.

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

Try to solve the constraints to be added.

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

Don't allow the argument to produce any constraints.

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

Guard constraint

wakeupConstraints :: MonadTCM tcm => tcm () | Source

We ignore the constraint ids and (as in Agda) retry all constraints every time. We probably generate very few constraints.

solveConstraints :: MonadTCM tcm => Constraints -> tcm Constraints | Source

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

Produced by Haddock version 2.4.2