| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 Constraints | Source

Compare two sizes. Only with --sized-types.

trivial :: MonadTCM tcm => Term -> Term -> tcm Bool | Source

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 |

Instances

Show SizeExpr

data SizeConstraint | Source

Constructors

Leq SizeExpr Int SizeExpr |

Instances

Show SizeConstraint

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 Bool | Source

solveSizeConstraints :: MonadTCM tcm => tcm () | Source

Produced by Haddock version 2.4.2