Agda.TypeChecking.SizedTypes
- compareSizes :: MonadTCM tcm => Comparison -> Term -> Term -> tcm Constraints
- trivial :: MonadTCM tcm => Term -> Term -> tcm Bool
- getSizeConstraints :: MonadTCM tcm => tcm [SizeConstraint]
- getSizeMetas :: MonadTCM tcm => tcm [(MetaId, Int)]
- data SizeExpr
- data SizeConstraint = Leq SizeExpr Int SizeExpr
- computeSizeConstraint :: MonadTCM tcm => ConstraintClosure -> tcm (Maybe SizeConstraint)
- sizeExpr :: MonadTCM tcm => Term -> tcm (SizeExpr, Int)
- flexibleVariables :: SizeConstraint -> [(MetaId, [CtxId])]
- haveSizedTypes :: MonadTCM tcm => tcm Bool
- solveSizeConstraints :: MonadTCM tcm => tcm ()
Documentation
compareSizes :: MonadTCM tcm => Comparison -> Term -> Term -> tcm ConstraintsSource
Compare two sizes. Only with --sized-types.
getSizeConstraints :: MonadTCM tcm => tcm [SizeConstraint]Source
Find the size constraints.
getSizeMetas :: MonadTCM tcm => tcm [(MetaId, Int)]Source
computeSizeConstraint :: MonadTCM tcm => ConstraintClosure -> tcm (Maybe SizeConstraint)Source
sizeExpr :: MonadTCM tcm => Term -> tcm (SizeExpr, Int)Source
Throws a patternViolation if the term isn't a proper size expression.
flexibleVariables :: SizeConstraint -> [(MetaId, [CtxId])]Source
haveSizedTypes :: MonadTCM tcm => tcm BoolSource
solveSizeConstraints :: MonadTCM tcm => tcm ()Source