Constraint package:Agda

Constraint: an inequation between size expressions, e.g. X < ∞ or i + 3 ≤ j.

Constraints :: ProfileOption

Agda Agda.Utils.ProfileOptions

Collect statistics about constraint solving

constraintProblems :: ProblemConstraint -> Set ProblemId

Agda Agda.TypeChecking.Monad.Base

constraintUnblocker :: ProblemConstraint -> Blocker

Agda Agda.TypeChecking.Monad.Base

constraintMetas :: Constraint -> TCM (Set MetaId)

Agda Agda.TypeChecking.Monad.MetaVars

Returns all metavariables in a constraint. Slightly complicated by the fact that blocked terms are represented by two meta variables. To find the second one we need to look up the meta listeners for the one in the UnBlock constraint. This is used for the purpose of deciding if a metavariable is constrained or if it can be generalized over (see Agda.TypeChecking.Generalize).

constraintGraph :: (Ord r, Ord f, Pretty r, Pretty f) => [Constraint' r f] -> HypGraph r f -> Either Error (ConGraph r f)

Agda Agda.TypeChecking.SizedTypes.WarshallSolver

constraintGraphs :: (Ord r, Ord f, Pretty r, Pretty f) => [Constraint' r f] -> HypGraph r f -> Either Error ([f], ConGraphs r f)

Agda Agda.TypeChecking.SizedTypes.WarshallSolver

Cmd_constraints :: Interaction' range

Agda Agda.Interaction.Base

data OutputConstraint' a b

Agda Agda.Interaction.Base

A subset of OutputConstraint.

data OutputConstraint_boot tcErr a b

Agda Agda.Interaction.Base

getConstraints :: TCM [OutputForm Expr Expr]