Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.SizedTypes
Synopsis
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
= SizeMeta MetaId [CtxId]
| Rigid CtxId
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.
trivial :: MonadTCM tcm => Term -> Term -> tcm BoolSource
getSizeConstraints :: MonadTCM tcm => tcm [SizeConstraint]Source
Find the size constraints.
getSizeMetas :: MonadTCM tcm => tcm [(MetaId, Int)]Source
data SizeExpr Source
Constructors
SizeMeta MetaId [CtxId]
Rigid CtxId
show/hide Instances
data SizeConstraint Source
Constructors
Leq SizeExpr Int SizeExpr
show/hide Instances
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
Produced by Haddock version 2.4.2