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