Constraint package:Agda

data Constraint
Agda Agda.Compiler.Backend Agda.TypeChecking.Monad.Base
module Agda.TypeChecking.Pretty.Constraint
Agda
Constraint :: SizeExpr' rigid flex -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Agda Agda.TypeChecking.SizedTypes.Syntax
type Constraint = Constraint' Rigid Flex
Agda Agda.TypeChecking.SizedTypes.Syntax
data Constraint
Agda Agda.Utils.Warshall
A constraint is an edge in the graph.
data ConstraintStatus
Agda Agda.Compiler.Backend Agda.TypeChecking.Monad.Constraints
type Constraints = [ProblemConstraint]
Agda Agda.Compiler.Backend Agda.TypeChecking.Monad.Base
module Agda.TypeChecking.Constraints
Agda
module Agda.TypeChecking.Monad.Constraints
Agda
data Constraint' rigid flex
Agda Agda.TypeChecking.SizedTypes.Syntax
Constraint: an inequation between size expressions, e.g. X < ∞ or i + 3 ≤ j.
Constraints :: ProfileOption
Agda Agda.Utils.ProfileOptions
Collect statistics about constraint solving
type Constraints = [Constraint]
Agda Agda.Utils.Warshall
constraintMetas :: Constraint -> TCM (Set MetaId)
Agda Agda.Compiler.Backend 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).
constraintProblems :: ProblemConstraint -> Set ProblemId
Agda Agda.Compiler.Backend Agda.TypeChecking.Monad.Base
constraintUnblocker :: ProblemConstraint -> Blocker
Agda Agda.Compiler.Backend Agda.TypeChecking.Monad.Base
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
AwakeConstraint :: ConstraintStatus
Agda Agda.Compiler.Backend
BuiltinAgdaTCMNoConstraints :: BuiltinId
Agda Agda.Compiler.Backend
CannotSolveSizeConstraints :: List1 (ProblemConstraint, HypSizeConstraint) -> Doc -> TypeError
Agda Agda.Compiler.Backend
The list of constraints is given redundantly as pairs of ProblemConstraint (original constraint) and HypSizeConstraint (form with size assumptions in context spelled out). The Doc is some extra reason for why solving failed.
CheckConstraint :: Nat -> ProblemConstraint -> Listener
Agda Agda.Compiler.Backend
ContradictorySizeConstraint :: (ProblemConstraint, HypSizeConstraint) -> TypeError
Agda Agda.Compiler.Backend
FaceConstraintCannotBeHidden :: ArgInfo -> Warning
Agda Agda.Compiler.Backend
Face constraint patterns (i = 0) must be visible arguments.
FaceConstraintCannotBeNamed :: NamedName -> Warning
Agda Agda.Compiler.Backend
Face constraint patterns (i = 0) must be unnamed arguments.
class (MonadTCEnv m, ReadTCState m, MonadError TCErr m, MonadBlock m, HasOptions m, MonadDebug m) => MonadConstraint m
Agda Agda.Compiler.Backend
Monad service class containing methods for adding and solving constraints