Agda-2.2.10: 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.6.1